for L being complete Lattice
for L9 being SubLattice of L st L9 is /\-inheriting holds
for A being Subset of L
for A9 being Subset of L9 st A = A9 holds
"/\" A = "/\" A9 by Th16;