let X be non empty TopSpace; :: thesis: ( X is almost_discrete implies X is hereditarily_extremally_disconnected )
assume X is almost_discrete ; :: thesis: X is hereditarily_extremally_disconnected
then reconsider X = X as non empty almost_discrete TopSpace ;
for X0 being non empty SubSpace of X holds X0 is extremally_disconnected by Th21, PRE_TOPC:22;
hence X is hereditarily_extremally_disconnected ; :: thesis: verum