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

A2: now

let c' be Element of ; :: thesis: ( c' is_less_than A' implies c' [= a' )
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 c' is_less_than A' ; :: thesis: c' [= a'
then c is_less_than A' by Th13;
then A3: c [= "/\" A',L by LATTICE3:34;
c' "/\" a' = c "/\" ("/\" A',L) by Th12
.= c' by A3, LATTICES:21 ;
hence c' [= a' by LATTICES:21; :: thesis: verum

end;

"/\" A',L is_less_than A' by LATTICE3:34;
then a' is_less_than A' by Th13;
hence "/\" A',L = "/\" A',L' by A2, LATTICE3:34; :: thesis: verum