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;
A2: now :: thesis: for c9 being Element of L91 st c9 is_less_than A9 holds
c9 [= a9
let c9 be Element of L91; :: thesis: ( c9 is_less_than A9 implies c9 [= a9 )
the carrier of L91 c= the carrier of L by NAT_LAT:def 12;
then reconsider c = c9 as Element of L ;
assume c9 is_less_than A9 ; :: thesis: c9 [= a9
then c is_less_than A9 by Th12;
then A3: c [= "/\" (A9,L) by LATTICE3:34;
c9 "/\" a9 = c "/\" ("/\" (A9,L)) by Th11
.= c9 by A3, LATTICES:4 ;
hence c9 [= a9 by LATTICES:4; :: thesis: verum
end;
"/\" (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; :: thesis: verum