let X be TopSpace; :: thesis: for A, B being Subset of X st A \/ B = the carrier of X holds
( ( A is closed implies A \/ (Int B) = the carrier of X ) & ( B is closed implies (Int A) \/ B = the carrier of X ) )
let A, B be Subset of X; :: thesis: ( A \/ B = the carrier of X implies ( ( A is closed implies A \/ (Int B) = the carrier of X ) & ( B is closed implies (Int A) \/ B = the carrier of X ) ) )
assume A \/ B = the carrier of X ; :: thesis: ( ( A is closed implies A \/ (Int B) = the carrier of X ) & ( B is closed implies (Int A) \/ B = the carrier of X ) )
then (A \/ B) ` = {} X by XBOOLE_1:37;
then (A ` ) /\ (B ` ) = {} by XBOOLE_1:53;
then A1: A ` misses B ` by XBOOLE_0:def 7;
thus ( A is closed implies A \/ (Int B) = the carrier of X ) :: thesis: ( B is closed implies (Int A) \/ B = the carrier of X )

proof

assume A is closed ; :: thesis: A \/ (Int B) = the carrier of X
then A ` is open ;
then A ` misses Cl (B ` ) by A1, TSEP_1:40;
then (A ` ) /\ (((Cl (B ` )) ` ) ` ) = {} by XBOOLE_0:def 7;
then (A ` ) /\ ((Int B) ` ) = {} by TOPS_1:def 1;
then (A \/ (Int B)) ` = {} X by XBOOLE_1:53;
then ((A \/ (Int B)) ` ) ` = [#] X ;
hence A \/ (Int B) = the carrier of X ; :: thesis: verum

end;

thus ( B is closed implies (Int A) \/ B = the carrier of X ) :: thesis: verum

proof

assume B is closed ; :: thesis: (Int A) \/ B = the carrier of X
then B ` is open ;
then Cl (A ` ) misses B ` by A1, TSEP_1:40;
then (((Cl (A ` )) ` ) ` ) /\ (B ` ) = {} by XBOOLE_0:def 7;
then ((Int A) ` ) /\ (B ` ) = {} by TOPS_1:def 1;
then ((Int A) \/ B) ` = {} X by XBOOLE_1:53;
then (((Int A) \/ B) ` ) ` = [#] X ;
hence (Int A) \/ B = the carrier of X ; :: thesis: verum

end;