let F be Field; :: thesis: for VS being strict VectSp of F holds lattice VS is complete
let VS be strict VectSp of F; :: thesis: lattice VS is complete
let Y be Subset of (lattice VS); :: according to VECTSP_8:def 6 :: thesis: 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 ) )

per cases ( Y = {} or Y <> {} ) ;
suppose A1: Y = {} ; :: thesis: 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 ) )

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: verum
proof
take Top (lattice VS) ; :: thesis: ( Top (lattice VS) is_less_than Y & ( for b being Element of (lattice VS) st b is_less_than Y holds
b [= Top (lattice VS) ) )

thus Top (lattice VS) is_less_than Y by A1; :: thesis: for b being Element of (lattice VS) st b is_less_than Y holds
b [= Top (lattice VS)

let b be Element of (lattice VS); :: thesis: ( b is_less_than Y implies b [= Top (lattice VS) )
assume b is_less_than Y ; :: thesis: b [= Top (lattice VS)
thus b [= Top (lattice VS) by LATTICES:19; :: thesis: verum
end;
end;
suppose Y <> {} ; :: thesis: 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 ) )

then reconsider X = Y as non empty Subset of () ;
reconsider p = meet X as Element of (lattice VS) by VECTSP_5:def 3;
take p ; :: thesis: ( p is_less_than Y & ( for b being Element of (lattice VS) st b is_less_than Y holds
b [= p ) )

set x = the Element of X;
thus p is_less_than Y :: thesis: for b being Element of (lattice VS) st b is_less_than Y holds
b [= p
proof
let q be Element of (lattice VS); :: according to LATTICE3:def 16 :: thesis: ( not q in Y or p [= q )
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: p [= q
(carr VS) . h = the carrier of H by ;
then meet ((carr VS) .: X) c= the carrier of H by ;
then the carrier of (meet X) c= the carrier of H by Def5;
hence p [= q by ; :: thesis: verum
end;
let r be Element of (lattice VS); :: thesis: ( r is_less_than Y implies r [= p )
consider H being strict Subspace of VS such that
A4: H = r by VECTSP_5:def 3;
assume A5: r is_less_than Y ; :: thesis: r [= p
A6: for Z1 being set st Z1 in (carr VS) .: X holds
the carrier of H c= Z1
proof
let Z1 be set ; :: thesis: ( Z1 in (carr VS) .: X implies the carrier of H c= Z1 )
assume A7: Z1 in (carr VS) .: X ; :: thesis: the carrier of H c= Z1
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 ;
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 ;
hence the carrier of H c= Z1 by A4, A11, A10, Th6; :: thesis: verum
end;
(carr VS) . the Element of X in (carr VS) .: X by FUNCT_2:35;
then the carrier of H c= meet ((carr VS) .: X) by ;
then the carrier of H c= the carrier of (meet X) by Def5;
hence r [= p by ; :: thesis: verum
end;
end;