let L be complete Lattice; :: thesis: for L' being SubLattice of L st L' is /\-inheriting holds
for A' being Subset of L' holds "/\" A',L = "/\" A',L'
let L' be SubLattice of L; :: thesis: ( L' is /\-inheriting implies for A' being Subset of L' holds "/\" A',L = "/\" A',L' )
assume A1: L' is /\-inheriting ; :: thesis: for A' being Subset of L' holds "/\" A',L = "/\" A',L'
then reconsider L'1 = L' as complete SubLattice of L ;
let A' be Subset of L'; :: thesis: "/\" A',L = "/\" A',L'
set a = "/\" A',L;
reconsider a' = "/\" A',L as Element of L'1 by A1, Def2;
( "/\" A',L is_less_than A' & ( for c being Element of L st c is_less_than A' holds
c [= "/\" A',L ) ) by LATTICE3:34;
then A2: a' is_less_than A' by Th13;

now

let c' be Element of L'1; :: 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 L 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;

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