for T being 1-sorted
for A, B being Subset of T holds
( A misses B iff B c= A ` ) by SUBSET_1:23;