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