:: deftheorem defines misses TSEP_1:def 3 :
for X1, X2 being 1-sorted holds
( X1 misses X2 iff the carrier of X1 misses the carrier of X2 );