-interpretation "Ordered set upper bound" 'upper_bound s x =
- (cic:/matita/dama/supremum/upper_bound.con _ s x).
-interpretation "Ordered set lower bound" 'lower_bound s x =
- (cic:/matita/dama/supremum/lower_bound.con _ s x).
-interpretation "Ordered set increasing" 'increasing s =
- (cic:/matita/dama/supremum/increasing.con _ s).
-interpretation "Ordered set decreasing" 'decreasing s =
- (cic:/matita/dama/supremum/decreasing.con _ s).
-interpretation "Ordered set strong sup" 'supremum s x =
- (cic:/matita/dama/supremum/supremum.con _ s x).
-interpretation "Ordered set strong inf" 'infimum s x =
- (cic:/matita/dama/supremum/infimum.con _ s x).
+interpretation "Ordered set upper bound" 'upper_bound s x = (upper_bound _ s x).
+interpretation "Ordered set lower bound" 'lower_bound s x = (lower_bound _ s x).
+interpretation "Ordered set increasing" 'increasing s = (increasing _ s).
+interpretation "Ordered set decreasing" 'decreasing s = (decreasing _ s).
+interpretation "Ordered set strong sup" 'supremum s x = (supremum _ s x).
+interpretation "Ordered set strong inf" 'infimum s x = (infimum _ s x).