theorem :: MSUALG_7:19

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 Th17;