let X be TopSpace; :: thesis: for A1, A2 being Subset of X st A1 \/ A2 is closed & A1,A2 are_separated holds
( A1 is closed & A2 is closed )
let A1, A2 be Subset of X; :: thesis: ( A1 \/ A2 is closed & A1,A2 are_separated implies ( A1 is closed & A2 is closed ) )
assume A1: A1 \/ A2 is closed ; :: thesis: ( not A1,A2 are_separated or ( A1 is closed & A2 is closed ) )
then Cl A1 c= A1 \/ A2 by TOPS_1:5, XBOOLE_1:7;
then A2: (Cl A1) \ A2 c= A1 by XBOOLE_1:43;
assume A3: A1,A2 are_separated ; :: thesis: ( A1 is closed & A2 is closed )
then Cl A1 misses A2 by CONNSP_1:def 1;
then A4: Cl A1 c= A1 by A2, XBOOLE_1:83;
Cl A2 c= A1 \/ A2 by A1, TOPS_1:5, XBOOLE_1:7;
then A5: (Cl A2) \ A1 c= A2 by XBOOLE_1:43;
Cl A2 misses A1 by A3, CONNSP_1:def 1;
then A6: Cl A2 c= A2 by A5, XBOOLE_1:83;
( A1 c= Cl A1 & A2 c= Cl A2 ) by PRE_TOPC:18;
hence ( A1 is closed & A2 is closed ) by A6, A4, XBOOLE_0:def 10; :: thesis: verum