-interpretation "Ordered field le" 'leq a b =
- (cic:/matita/ordered_fields_ch0/of_le.con _ a b).
-
-definition lt \def λF:ordered_field_ch0.λa,b:F.a ≤ b ∧ a ≠ b.
+(*theorem ordered_set_of_ordered_field_ch0:
+ ∀F:ordered_field_ch0.ordered_set F.
+ intros;
+ apply mk_ordered_set;
+ [ apply (mk_pre_ordered_set ? (of_le F))
+ | apply mk_is_order_relation;
+ [ apply (of_reflexive F)
+ | apply antisimmetric_to_cotransitive_to_transitive;
+ [ apply (of_antisimmetric F)
+ | apply (of_cotransitive F)
+ ]
+ | apply (of_antisimmetric F)
+ ]
+ ].
+qed.