consider X being non empty strict discrete TopSpace;
take X ; :: thesis: ( X is hereditarily_extremally_disconnected & X is strict )

now

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

now

let A be Subset of ; :: thesis: ( A is open implies Cl A is open )
assume A1: A is open ; :: thesis: Cl A is open
A is closed by Th18;
hence Cl A is open by A1, PRE_TOPC:52; :: thesis: verum

end;

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

end;

hence ( X is hereditarily_extremally_disconnected & X is strict ) by Def5; :: thesis: verum