:: deftheorem Def4 defines extremally_disconnected TDLAT_3:def 4 :
for IT being non empty TopSpace holds
( IT is extremally_disconnected iff for A being Subset of IT st A is open holds
Cl A is open );