let X be TopSpace; :: thesis: for A, B being Subset of X st A \/ B = the carrier of X & A is closed holds
A \/ (Int B) = the carrier of X
let A, B be Subset of X; :: thesis: ( A \/ B = the carrier of X & A is closed implies A \/ (Int B) = the carrier of X )
assume A \/ B = the carrier of X ; :: thesis: ( not A is closed or A \/ (Int 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 ` ;
assume A is closed ; :: thesis: A \/ (Int B) = the carrier of X
then A ` misses Cl (B `) by A1, TSEP_1:36;
then (A `) /\ (((Cl (B `)) `) `) = {} ;
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