theorem Th9: :: JORDAN24:9
for X being set
for A being Subset of X holds
( A ` = {} iff A = X ) by XBOOLE_1:37;