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

proof

let X be Subset of L9; :: thesis:
set a = "/\" (X,L);
reconsider a9 = "/\" (X,L) as Element of L9 by A1;
take a9 ; :: thesis:
"/\" (X,L) is_less_than X by LATTICE3:34;
hence a9 is_less_than X by Th12; :: thesis:
let b9 be Element of L9; :: thesis:
the carrier of L9 c= the carrier of L by NAT_LAT:def 12;
then reconsider b = b9 as Element of L ;
assume b9 is_less_than X ; :: thesis:
then b is_less_than X by Th12;
then A2: b [= "/\" (X,L) by LATTICE3:39;
b9 "/\" a9 = b "/\" ("/\" (X,L)) by Th11
.= b9 by A2, LATTICES:4 ;
hence b9 [= a9 by LATTICES:4; :: thesis:

end;

hence L9 is complete by VECTSP_8:def 6; :: thesis: