let X be non empty TopSpace; :: thesis: ( X is extremally_disconnected iff for A, B being Subset of X st A is closed & B is closed & A \/ B = the carrier of X holds
(Int A) \/ (Int B) = the carrier of X )
thus ( X is extremally_disconnected implies for A, B being Subset of X st A is closed & B is closed & A \/ B = the carrier of X holds
(Int A) \/ (Int B) = the carrier of X ) :: thesis: ( ( for A, B being Subset of X st A is closed & B is closed & A \/ B = the carrier of X holds
(Int A) \/ (Int B) = the carrier of X ) implies X is extremally_disconnected )

proof

assume A1: X is extremally_disconnected ; :: thesis: for A, B being Subset of X st A is closed & B is closed & A \/ B = the carrier of X holds
(Int A) \/ (Int B) = the carrier of X
let A, B be Subset of X; :: thesis: ( A is closed & B is closed & A \/ B = the carrier of X implies (Int A) \/ (Int B) = the carrier of X )
assume that
A2: A is closed and
A3: B is closed ; :: thesis: ( not A \/ B = the carrier of X or (Int A) \/ (Int B) = the carrier of X )
assume A \/ B = the carrier of X ; :: thesis: (Int A) \/ (Int B) = the carrier of X
then (A \/ B) ` = {} X by XBOOLE_1:37;
then (A ` ) /\ (B ` ) = {} X by XBOOLE_1:53;
then A ` misses B ` by XBOOLE_0:def 7;
then Cl (A ` ) misses Cl (B ` ) by A1, A2, A3, Th30;
then (Cl (A ` )) /\ (Cl (B ` )) = {} X by XBOOLE_0:def 7;
then ((Cl (A ` )) /\ (Cl (B ` ))) ` = [#] X ;
then ((Cl (A ` )) ` ) \/ ((Cl (B ` )) ` ) = [#] X by XBOOLE_1:54;
then ((Cl (A ` )) ` ) \/ (Int B) = [#] X by TOPS_1:def 1;
hence (Int A) \/ (Int B) = the carrier of X by TOPS_1:def 1; :: thesis: verum

end;

assume A4: for A, B being Subset of X st A is closed & B is closed & A \/ B = the carrier of X holds
(Int A) \/ (Int B) = the carrier of X ; :: thesis: X is extremally_disconnected

now

let A, B be Subset of X; :: thesis: ( A is open & B is open & A misses B implies Cl A misses Cl B )
assume that
A5: A is open and
A6: B is open ; :: thesis: ( A misses B implies Cl A misses Cl B )
assume A misses B ; :: thesis: Cl A misses Cl B
then A /\ B = {} X by XBOOLE_0:def 7;
then (A /\ B) ` = [#] X ;
then (A ` ) \/ (B ` ) = [#] X by XBOOLE_1:54;
then (Int (A ` )) \/ (Int (B ` )) = the carrier of X by A4, A5, A6;
then ((Int (A ` )) \/ (Int (B ` ))) ` = {} X by XBOOLE_1:37;
then ((Int (A ` )) ` ) /\ ((Int (B ` )) ` ) = {} X by XBOOLE_1:53;
then (Cl A) /\ ((Int (B ` )) ` ) = {} X by Th2;
then Cl A misses (Int (B ` )) ` by XBOOLE_0:def 7;
hence Cl A misses Cl B by Th2; :: thesis: verum

end;

hence X is extremally_disconnected by Th30; :: thesis: verum