for L being complete Lattice
for L9 being SubLattice of L st L9 is \/-inheriting holds
for A9 being Subset of L9 holds "\/" (A9,L) = "\/" (A9,L9)