theorem Th23: :: SUBSET_1:23

for E being set
for A, B being Subset of E holds
( A misses B iff A c= B ` )