:: deftheorem Def5 defines hereditarily_extremally_disconnected TDLAT_3:def 5 :
for IT being non empty TopSpace holds
( IT is hereditarily_extremally_disconnected iff for X0 being non empty SubSpace of IT holds X0 is extremally_disconnected );