:: deftheorem defines c= LATTICE7:def 1 :
for L being 1-sorted
for A, B being Subset of L holds
( A c= B iff for x being Element of L st x in A holds
x in B );