let F be Field; :: thesis:
let VS be strict VectSp of F; :: thesis:
let Y be Subset of (lattice VS); :: according to VECTSP_8:def 6 :: thesis:

thus ex a being Element of (lattice VS) st
( a is_less_than Y & ( for b being Element of (lattice VS) st b is_less_than Y holds
b [= a ) ) :: thesis:

end;

then reconsider X = Y as non empty Subset of (Subspaces VS) ;
reconsider p = meet X as Element of (lattice VS) by VECTSP_5:def 3;
take p ; :: thesis:
set x = the Element of X;
thus p is_less_than Y :: thesis:

let q be Element of (lattice VS); :: according to LATTICE3:def 16 :: thesis:
consider H being strict Subspace of VS such that
A2: H = q by VECTSP_5:def 3;
reconsider h = q as Element of Subspaces VS ;
assume A3: q in Y ; :: thesis:
(carr VS) . h = the carrier of H by A2, Def4;
then meet ((carr VS) .: X) c= the carrier of H by A3, FUNCT_2:35, SETFAM_1:3;
then the carrier of (meet X) c= the carrier of H by Def5;
hence p [= q by A2, Th6; :: thesis:

end;

let Z1 be set ; :: thesis:
assume A7: Z1 in (carr VS) .: X ; :: thesis:
then reconsider Z2 = Z1 as Subset of VS ;
consider z1 being Element of Subspaces VS such that
A8: z1 in X and
A9: Z2 = (carr VS) . z1 by A7, FUNCT_2:65;
reconsider z1 = z1 as Element of (lattice VS) ;
A10: r [= z1 by A5, A8;
consider z3 being strict Subspace of VS such that
A11: z3 = z1 by VECTSP_5:def 3;
Z1 = the carrier of z3 by A9, A11, Def4;
hence the carrier of H c= Z1 by A4, A11, A10, Th6; :: thesis:

end;

end;