let L be complete Lattice; 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; ( L9 is /\-inheriting implies for A9 being Subset of L9 holds "/\" (A9,L) = "/\" (A9,L9) )
assume A1:
L9 is /\-inheriting
; 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; "/\" (A9,L) = "/\" (A9,L9)
set a = "/\" (A9,L);
reconsider a9 = "/\" (A9,L) as Element of L91 by A1;
"/\" (A9,L) is_less_than A9
by LATTICE3:34;
then
a9 is_less_than A9
by Th12;
hence
"/\" (A9,L) = "/\" (A9,L9)
by A2, LATTICE3:34; verum