let X be TopStruct ; :: thesis: for A being Subset of X holds
( ( A = {} X implies A ` = [#] X ) & ( A ` = [#] X implies A = {} X ) & ( A = {} implies A ` = the carrier of X ) & ( A ` = the carrier of X implies A = {} ) )
let A be Subset of X; :: thesis: ( ( A = {} X implies A ` = [#] X ) & ( A ` = [#] X implies A = {} X ) & ( A = {} implies A ` = the carrier of X ) & ( A ` = the carrier of X implies A = {} ) )
thus ( A = {} X iff A ` = [#] X ) :: thesis: ( A = {} iff A ` = the carrier of X )
proof
thus ( A = {} X implies A ` = [#] X ) ; :: thesis: ( A ` = [#] X implies A = {} X )
assume A ` = [#] X ; :: thesis: A = {} X
then (A `) ` = {} X by XBOOLE_1:37;
hence A = {} X ; :: thesis: verum
end;
hence ( A = {} iff A ` = the carrier of X ) ; :: thesis: verum