set X = the non empty strict discrete TopSpace;
take the non empty strict discrete TopSpace ; :: thesis: ( the non empty strict discrete TopSpace is hereditarily_extremally_disconnected & the non empty strict discrete TopSpace is strict )

now

let X0 be non empty SubSpace of the non empty strict discrete TopSpace; :: thesis: X0 is extremally_disconnected

now

let A be Subset of X0; :: 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:22; :: thesis: verum

end;

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

end;

hence ( the non empty strict discrete TopSpace is hereditarily_extremally_disconnected & the non empty strict discrete TopSpace is strict ) by Def5; :: thesis: verum