for X being non empty extremally_disconnected TopSpace
for X0 being non empty SubSpace of X
for A being Subset of X st A = the carrier of X0 & A is dense holds
X0 is extremally_disconnected