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 )
for A being Subset of the non empty strict discrete TopSpace st A is open holds
Cl A is open by PRE_TOPC:22, Th16;
hence ( the non empty strict discrete TopSpace is extremally_disconnected & the non empty strict discrete TopSpace is strict ) ; :: thesis: verum