let X be set ; :: thesis: for A being Subset of X holds
( A ` = {} iff A = X )
let A be Subset of X; :: thesis: ( A ` = {} iff A = X )
( {} = {} X & [#] X = X & (A ` ) ` = A ) ;
hence ( A ` = {} iff A = X ) by XBOOLE_1:37; :: thesis: verum