theorem Th13: :: MSUALG_7:13

for L being Lattice
for L9 being SubLattice of L
for X being Subset of L9
for a being Element of L
for a9 being Element of L9 st a = a9 holds
( X is_less_than a iff X is_less_than a9 )