:: deftheorem defines includes_lattice_of COHSP_1:def 8 :
for X, x, y being set holds
( X includes_lattice_of x,y iff X includes_lattice_of {x,y} );