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