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, Def3;

A2: now

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 16;
then reconsider c = c9 as Element of L by TARSKI:def 3;
assume A9 is_less_than c9 ; :: thesis: a9 [= c9
then A9 is_less_than c by Th14;
then A3: "\/" A9,L [= c by LATTICE3:def 21;
a9 "/\" c9 = ("\/" A9,L) "/\" c by Th12
.= a9 by A3, LATTICES:21 ;
hence a9 [= c9 by LATTICES:21; :: thesis: verum

end;

A9 is_less_than "\/" A9,L by LATTICE3:def 21;
then A9 is_less_than a9 by Th14;
hence "\/" A9,L = "\/" A9,L9 by A2, LATTICE3:def 21; :: thesis: verum