let S be 1-sorted ; :: thesis: for X being Subset of S holds
( X ` = the carrier of S iff X is empty )
let X be Subset of S; :: thesis: ( X ` = the carrier of S iff X is empty )
hereby :: thesis: ( X is empty implies X ` = the carrier of S )
assume X ` = the carrier of S ; :: thesis: X is empty
then X = ([#] the carrier of S) ` ;
hence X is empty by XBOOLE_1:37; :: thesis: verum
end;
assume X is empty ; :: thesis: X ` = the carrier of S
hence X ` = the carrier of S ; :: thesis: verum