let X be non empty TopSpace; :: thesis: ( X is hereditarily_extremally_disconnected implies X is extremally_disconnected )
assume A1: X is hereditarily_extremally_disconnected ; :: thesis: X is extremally_disconnected
X is SubSpace of X by TSEP_1:2;
hence X is extremally_disconnected by A1; :: thesis: verum