for X being non empty TopSpace holds
( X is extremally_disconnected iff for A being Subset of X holds
( ( A is open_condensed implies A is closed_condensed ) & ( A is closed_condensed implies A is open_condensed ) ) )