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 ;

now

let X0 be non empty SubSpace of X; :: thesis: X0 is extremally_disconnected

now

let A be Subset of X0; :: thesis: ( A is open implies Cl A is open )
assume A2: A is open ; :: thesis: Cl A is open
then A is closed by Th23;
hence Cl A is open by A2, PRE_TOPC:22; :: thesis: verum

end;

hence X0 is extremally_disconnected by Def4; :: thesis: verum

end;

hence X is hereditarily_extremally_disconnected by Def5; :: thesis: verum