let X be non empty TopSpace; :: thesis: ( ( for X0 being non empty closed SubSpace of X holds X0 is extremally_disconnected ) implies X is hereditarily_extremally_disconnected )
assume A1: for Y being non empty closed SubSpace of X holds Y is extremally_disconnected ; :: thesis: X is hereditarily_extremally_disconnected
for X0 being non empty SubSpace of X holds X0 is extremally_disconnected
proof
let X0 be non empty SubSpace of X; :: thesis: X0 is extremally_disconnected
reconsider A0 = the carrier of X0 as Subset of X by TSEP_1:1;
set A = Cl A0;
not Cl A0 is empty by PCOMPS_1:2;
then consider Y being non empty strict closed SubSpace of X such that
A2: Cl A0 = the carrier of Y by TSEP_1:15;
A0 c= Cl A0 by PRE_TOPC:18;
then reconsider Y0 = X0 as non empty SubSpace of Y by A2, TSEP_1:4;
reconsider B0 = the carrier of Y0 as Subset of Y by TSEP_1:1;
Cl B0 = (Cl A0) /\ ([#] Y) by PRE_TOPC:17;
then A3: B0 is dense by A2, TOPS_1:def 3;
Y is extremally_disconnected by A1;
hence X0 is extremally_disconnected by A3, Th37; :: thesis: verum
end;
hence X is hereditarily_extremally_disconnected ; :: thesis: verum