theorem Th1: :: TOPGEN_1:1

for T being 1-sorted
for A, B being Subset of T holds
( A meets B ` iff A \ B <> {} ) by SUBSET_1:13;