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 )
(A `) ` = A ;
hence ( A ` = {} iff A = X ) by XBOOLE_1:37; :: thesis: verum