theorem Th16: :: COHSP_1:16

for X, x, y being set holds
( X includes_lattice_of x,y iff ( x in X & y in X & x /\ y in X & x \/ y in X ) )