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

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

a [= b ) )

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

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

a [= b ) )

proof

hence
L9 is complete
; :: thesis: verum
let X be Subset of L9; :: thesis: ex a being Element of L9 st

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

a [= b ) )

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

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

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

a9 [= b ) )

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

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

a9 [= b

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

the carrier of L9 c= the carrier of L by NAT_LAT:def 12;

then reconsider b = b9 as Element of L ;

assume X is_less_than b9 ; :: thesis: a9 [= b9

then X is_less_than b by Th13;

then A2: "\/" (X,L) [= b by LATTICE3:def 21;

a9 "/\" b9 = ("\/" (X,L)) "/\" b by Th11

.= a9 by A2, LATTICES:4 ;

hence a9 [= b9 by LATTICES:4; :: thesis: verum

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

a [= b ) )

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

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

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

a9 [= b ) )

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

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

a9 [= b

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

the carrier of L9 c= the carrier of L by NAT_LAT:def 12;

then reconsider b = b9 as Element of L ;

assume X is_less_than b9 ; :: thesis: a9 [= b9

then X is_less_than b by Th13;

then A2: "\/" (X,L) [= b by LATTICE3:def 21;

a9 "/\" b9 = ("\/" (X,L)) "/\" b by Th11

.= a9 by A2, LATTICES:4 ;

hence a9 [= b9 by LATTICES:4; :: thesis: verum