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 \/ A2 is closed ; :: thesis: ( not A1,A2 are_separated or ( A1 is closed & A2 is closed ) )
then ( Cl A1 c= A1 \/ A2 & Cl A2 c= A1 \/ A2 ) by TOPS_1:31, XBOOLE_1:7;
then A1: ( (Cl A1) \ A2 c= A1 & (Cl A2) \ A1 c= A2 ) by XBOOLE_1:43;
assume A1,A2 are_separated ; :: thesis: ( A1 is closed & A2 is closed )
then ( Cl A1 misses A2 & Cl A2 misses A1 ) by CONNSP_1:def 1;
then ( Cl A2 c= A2 & Cl A1 c= A1 & A1 c= Cl A1 & A2 c= Cl A2 ) by A1, PRE_TOPC:48, XBOOLE_1:83;
hence ( A1 is closed & A2 is closed ) by XBOOLE_0:def 10; :: thesis: verum