let X0 be non empty SubSpace of X; :: thesis: ( X0 is open implies X0 is extremally_disconnected )
assume A1: X0 is open ; :: thesis: X0 is extremally_disconnected
reconsider B = the carrier of X0 as Subset of X by TSEP_1:1;

now :: thesis: for A0 being Subset of X0 st A0 is open holds
Cl A0 is open

let A0 be Subset of X0; :: thesis: ( A0 is open implies Cl A0 is open )
A0 c= B ;
then reconsider A = A0 as Subset of X by XBOOLE_1:1;
assume A0 is open ; :: thesis: Cl A0 is open
then A is open by A1, TSEP_1:17;
then A2: Cl A is open by Def4;
Cl A0 = (Cl A) /\ ([#] X0) by PRE_TOPC:17;
hence Cl A0 is open by A2, TOPS_2:24; :: thesis: verum

end;

hence X0 is extremally_disconnected ; :: thesis: verum