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

for A9 being Subset of L9 holds "\/" (A9,L) = "\/" (A9,L9)

let L9 be SubLattice of L; :: thesis: ( L9 is \/-inheriting implies for A9 being Subset of L9 holds "\/" (A9,L) = "\/" (A9,L9) )

assume A1: L9 is \/-inheriting ; :: thesis: for A9 being Subset of L9 holds "\/" (A9,L) = "\/" (A9,L9)

then reconsider L91 = L9 as complete SubLattice of L ;

let A9 be Subset of L9; :: thesis: "\/" (A9,L) = "\/" (A9,L9)

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

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

then A9 is_less_than a9 by Th13;

hence "\/" (A9,L) = "\/" (A9,L9) by A2, LATTICE3:def 21; :: thesis: verum

for A9 being Subset of L9 holds "\/" (A9,L) = "\/" (A9,L9)

let L9 be SubLattice of L; :: thesis: ( L9 is \/-inheriting implies for A9 being Subset of L9 holds "\/" (A9,L) = "\/" (A9,L9) )

assume A1: L9 is \/-inheriting ; :: thesis: for A9 being Subset of L9 holds "\/" (A9,L) = "\/" (A9,L9)

then reconsider L91 = L9 as complete SubLattice of L ;

let A9 be Subset of L9; :: thesis: "\/" (A9,L) = "\/" (A9,L9)

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

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

A2: now :: thesis: for c9 being Element of L91 st A9 is_less_than c9 holds

a9 [= c9

A9 is_less_than "\/" (A9,L)
by LATTICE3:def 21;a9 [= c9

let c9 be Element of L91; :: thesis: ( A9 is_less_than c9 implies a9 [= c9 )

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

then reconsider c = c9 as Element of L ;

assume A9 is_less_than c9 ; :: thesis: a9 [= c9

then A9 is_less_than c by Th13;

then A3: "\/" (A9,L) [= c by LATTICE3:def 21;

a9 "/\" c9 = ("\/" (A9,L)) "/\" c by Th11

.= a9 by A3, LATTICES:4 ;

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

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

then reconsider c = c9 as Element of L ;

assume A9 is_less_than c9 ; :: thesis: a9 [= c9

then A9 is_less_than c by Th13;

then A3: "\/" (A9,L) [= c by LATTICE3:def 21;

a9 "/\" c9 = ("\/" (A9,L)) "/\" c by Th11

.= a9 by A3, LATTICES:4 ;

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

then A9 is_less_than a9 by Th13;

hence "\/" (A9,L) = "\/" (A9,L9) by A2, LATTICE3:def 21; :: thesis: verum