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 :: thesis: for X0 being non empty SubSpace of the non empty strict discrete TopSpace holds X0 is extremally_disconnected

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

now :: thesis: for A being Subset of X0 st A is open holds
Cl A is open

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 Th16;
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