let X be TopSpace; :: thesis: for A1, A2 being Subset of X st A1 \/ A2 is open & A1,A2 are_separated holds
( A1 is open & A2 is open )
let A1, A2 be Subset of X; :: thesis: ( A1 \/ A2 is open & A1,A2 are_separated implies ( A1 is open & A2 is open ) )
assume A1: A1 \/ A2 is open ; :: thesis: ( not A1,A2 are_separated or ( A1 is open & A2 is open ) )
A2: ( A1 c= Cl A1 & A2 c= Cl A2 ) by PRE_TOPC:48;
assume A1,A2 are_separated ; :: thesis: ( A1 is open & A2 is open )
then ( A2 misses Cl A1 & A1 misses Cl A2 ) by CONNSP_1:def 1;
then A3: ( A2 c= (Cl A1) ` & A1 c= (Cl A2) ` ) by SUBSET_1:43;
A4: (A1 \/ A2) /\ ((Cl A1) ` ) = (A1 \/ A2) \ (Cl A1) by SUBSET_1:32
.= (A1 \ (Cl A1)) \/ (A2 \ (Cl A1)) by XBOOLE_1:42
.= {} \/ (A2 \ (Cl A1)) by A2, XBOOLE_1:37
.= A2 /\ ((Cl A1) ` ) by SUBSET_1:32
.= A2 by A3, XBOOLE_1:28 ;
(A1 \/ A2) /\ ((Cl A2) ` ) = (A1 \/ A2) \ (Cl A2) by SUBSET_1:32
.= (A1 \ (Cl A2)) \/ (A2 \ (Cl A2)) by XBOOLE_1:42
.= (A1 \ (Cl A2)) \/ {} by A2, XBOOLE_1:37
.= A1 /\ ((Cl A2) ` ) by SUBSET_1:32
.= A1 by A3, XBOOLE_1:28 ;
hence ( A1 is open & A2 is open ) by A1, A4, TOPS_1:38; :: thesis: verum