-definition le \def λC:Type.λL:lattice C.λf,g. meet ? L f g = f.
-
-interpretation "Lattice le" 'leq a b =
- (cic:/matita/integration_algebras/le.con _ _ a b).
+lemma rs_lattice: ∀K:ordered_field_ch0.pre_riesz_space K → lattice.
+ intros (K V);
+ apply mk_lattice;
+ [ apply (carrier V)
+ | apply (eq_rect ? ? (λC:Type.C→C→C) ? ? (rs_with ? V));
+ apply l_join
+ | apply (eq_rect ? ? (λC:Type.C→C→C) ? ? (rs_with ? V));
+ apply l_meet
+ | apply
+ (eq_rect' ? ?
+ (λa:Type.λH:os_carrier (rs_lattice_ ? V)=a.
+ is_lattice a
+ (eq_rect Type (rs_lattice_ K V) (λC:Type.C→C→C)
+ (l_join (rs_lattice_ K V)) a H)
+ (eq_rect Type (rs_lattice_ K V) (λC:Type.C→C→C)
+ (l_meet (rs_lattice_ K V)) a H))
+ ? ? (rs_with ? V));
+ simplify;
+ apply l_lattice_properties
+ ].
+qed.