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