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
( X is_less_than a & ( for b being Element of L' st X is_less_than b holds
a [= b ) )

proof

let X be Subset of L'; :: thesis: ex a being Element of L' st
( X is_less_than a & ( for b being Element of L' st X is_less_than b holds
a [= b ) )
set a = "\/" X,L;
reconsider a' = "\/" X,L as Element of L' by A1, Def3;
take a' ; :: thesis: ( X is_less_than a' & ( for b being Element of L' st X is_less_than b holds
a' [= b ) )
X is_less_than "\/" X,L by LATTICE3:def 21;
hence X is_less_than a' by Th14; :: thesis: for b being Element of L' st X is_less_than b holds
a' [= b
let b' be Element of L'; :: thesis: ( X is_less_than b' implies a' [= b' )
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 X is_less_than b' ; :: thesis: a' [= b'
then X is_less_than b by Th14;
then A2: "\/" X,L [= b by LATTICE3:def 21;
a' "/\" b' = ("\/" X,L) "/\" b by Th12
.= a' by A2, LATTICES:21 ;
hence a' [= b' by LATTICES:21; :: thesis: verum

end;

hence L' is complete by Def1; :: thesis: verum