theorem Th4: :: PRE_TOPC:4

for T being 1-sorted
for P being Subset of T holds
( P <> [#] T iff ([#] T) \ P <> {} )