take X = the non empty strict discrete TopSpace; :: thesis: ( X is hereditarily_extremally_disconnected & X is strict )
for X0 being non empty SubSpace of X holds X0 is extremally_disconnected by Th16, PRE_TOPC:22;
hence ( X is hereditarily_extremally_disconnected & X is strict ) ; :: thesis: verum