set X0 = the non empty strict open SubSpace of X;
take the non empty strict open SubSpace of X ; :: thesis: ( the non empty strict open SubSpace of X is extremally_disconnected & the non empty strict open SubSpace of X is strict )
thus ( the non empty strict open SubSpace of X is extremally_disconnected & the non empty strict open SubSpace of X is strict ) ; :: thesis: verum