let L be complete Lattice; :: thesis: for L9 being SubLattice of L st L9 is /\-inheriting holds

L9 is complete

let L9 be SubLattice of L; :: thesis: ( L9 is /\-inheriting implies L9 is complete )

assume A1: L9 is /\-inheriting ; :: thesis: L9 is complete

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 ) )

L9 is complete

let L9 be SubLattice of L; :: thesis: ( L9 is /\-inheriting implies L9 is complete )

assume A1: L9 is /\-inheriting ; :: thesis: L9 is complete

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

hence
L9 is complete
by VECTSP_8:def 6; :: thesis: verum
let X be Subset of L9; :: thesis: 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 ) )

set a = "/\" (X,L);

reconsider a9 = "/\" (X,L) as Element of L9 by A1;

take a9 ; :: thesis: ( a9 is_less_than X & ( for b being Element of L9 st b is_less_than X holds

b [= a9 ) )

"/\" (X,L) is_less_than X by LATTICE3:34;

hence a9 is_less_than X by Th12; :: thesis: for b being Element of L9 st b is_less_than X holds

b [= a9

let b9 be Element of L9; :: thesis: ( b9 is_less_than X implies b9 [= a9 )

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: b9 [= a9

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: verum

end;( a is_less_than X & ( for b being Element of L9 st b is_less_than X holds

b [= a ) )

set a = "/\" (X,L);

reconsider a9 = "/\" (X,L) as Element of L9 by A1;

take a9 ; :: thesis: ( a9 is_less_than X & ( for b being Element of L9 st b is_less_than X holds

b [= a9 ) )

"/\" (X,L) is_less_than X by LATTICE3:34;

hence a9 is_less_than X by Th12; :: thesis: for b being Element of L9 st b is_less_than X holds

b [= a9

let b9 be Element of L9; :: thesis: ( b9 is_less_than X implies b9 [= a9 )

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: b9 [= a9

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: verum