let L be complete Lattice; :: thesis: for L' being SubLattice of L st L' is \/-inheriting holds
for A' being Subset of holds "\/" A',L = "\/" A',L'
let L' be SubLattice of L; :: thesis: ( L' is \/-inheriting implies for A' being Subset of holds "\/" A',L = "\/" A',L' )
assume A1: L' is \/-inheriting ; :: thesis: for A' being Subset of holds "\/" A',L = "\/" A',L'
then reconsider L'1 = L' as complete SubLattice of L ;
let A' be Subset of ; :: thesis: "\/" A',L = "\/" A',L'
set a = "\/" A',L;
reconsider a' = "\/" A',L as Element of by A1, Def3;

A2: now

let c' be Element of ; :: thesis: ( A' is_less_than c' implies a' [= c' )
the carrier of L'1 c= the carrier of L by NAT_LAT:def 16;
then reconsider c = c' as Element of by TARSKI:def 3;
assume A' is_less_than c' ; :: thesis: a' [= c'
then A' is_less_than c by Th14;
then A3: "\/" A',L [= c by LATTICE3:def 21;
a' "/\" c' = ("\/" A',L) "/\" c by Th12
.= a' by A3, LATTICES:21 ;
hence a' [= c' by LATTICES:21; :: thesis: verum

end;

A' is_less_than "\/" A',L by LATTICE3:def 21;
then A' is_less_than a' by Th14;
hence "\/" A',L = "\/" A',L' by A2, LATTICE3:def 21; :: thesis: verum