for L being complete Lattice
for L9 being SubLattice of L st L9 is \/-inheriting holds
L9 is complete