for X being non empty TopSpace st ( for X0 being non empty closed SubSpace of X holds X0 is extremally_disconnected ) holds
X is hereditarily_extremally_disconnected