:: deftheorem defines includes_lattice_of COHSP_1:def 7 :
for X, Y being set holds
( X includes_lattice_of Y iff for a, b being set st a in Y & b in Y holds
( a /\ b in X & a \/ b in X ) );