let L be complete Lattice; :: thesis: for L' being SubLattice of L st L' is /\-inheriting holds
L' is complete
let L' be SubLattice of L; :: thesis: ( L' is /\-inheriting implies L' is complete )
assume A1: L' is /\-inheriting ; :: thesis: L' is complete
for X being Subset of L' ex a being Element of L' st
( a is_less_than X & ( for b being Element of L' st b is_less_than X holds
b [= a ) )

proof

let X be Subset of L'; :: thesis: ex a being Element of L' st
( a is_less_than X & ( for b being Element of L' st b is_less_than X holds
b [= a ) )
set a = "/\" X,L;
reconsider a' = "/\" X,L as Element of L' by A1, Def2;
take a' ; :: thesis: ( a' is_less_than X & ( for b being Element of L' st b is_less_than X holds
b [= a' ) )
"/\" X,L is_less_than X by LATTICE3:34;
hence a' is_less_than X by Th13; :: thesis: for b being Element of L' st b is_less_than X holds
b [= a'
let b' be Element of L'; :: thesis: ( b' is_less_than X implies b' [= a' )
the carrier of L' c= the carrier of L by NAT_LAT:def 16;
then reconsider b = b' as Element of L by TARSKI:def 3;
assume b' is_less_than X ; :: thesis: b' [= a'
then b is_less_than X by Th13;
then A2: b [= "/\" X,L by LATTICE3:40;
b' "/\" a' = b "/\" ("/\" X,L) by Th12
.= b' by A2, LATTICES:21 ;
hence b' [= a' by LATTICES:21; :: thesis: verum

end;

hence L' is complete by VECTSP_8:def 6; :: thesis: verum