for X being TopStruct
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 = {} ) )