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