let X be TopStruct ; :: thesis: for A being Subset of X holds
( ( A = [#] X implies A ` = {} X ) & ( A ` = {} X implies A = [#] X ) & ( A = the carrier of X implies A ` = {} ) & ( A ` = {} implies A = the carrier of X ) )
let A be Subset of X; :: thesis: ( ( A = [#] X implies A ` = {} X ) & ( A ` = {} X implies A = [#] X ) & ( A = the carrier of X implies A ` = {} ) & ( A ` = {} implies A = the carrier of X ) )
thus ( A = [#] X iff A ` = {} X ) :: thesis: ( A = the carrier of X iff A ` = {} )

proof

thus ( A = [#] X implies A ` = {} X ) by XBOOLE_1:37; :: thesis: ( A ` = {} X implies A = [#] X )
assume A ` = {} X ; :: thesis: A = [#] X
then (A `) ` = [#] X ;
hence A = [#] X ; :: thesis: verum

end;

hence ( A = the carrier of X iff A ` = {} ) ; :: thesis: verum