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

now

let A be Subset of the non empty strict discrete TopSpace; :: 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 ( the non empty strict discrete TopSpace is extremally_disconnected & the non empty strict discrete TopSpace is strict ) by Def4; :: thesis: verum