theorem Th2: :: TDLAT_1:2

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