let X0 be non empty SubSpace of X; :: thesis: X0 is hereditarily_extremally_disconnected
for Y being non empty SubSpace of X0 holds Y is extremally_disconnected
proof
let Y be non empty SubSpace of X0; :: thesis: Y is extremally_disconnected
Y is SubSpace of X by TSEP_1:7;
hence Y is extremally_disconnected by Def5; :: thesis: verum
end;
hence X0 is hereditarily_extremally_disconnected ; :: thesis: verum