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 by PRE_TOPC:18;
assume A3: A1,A2 are_separated ; :: thesis: ( A1 is open & A2 is open )
then A2 misses Cl A1 by CONNSP_1:def 1;
then A4: A2 c= (Cl A1) ` by SUBSET_1:23;
A1 misses Cl A2 by A3, CONNSP_1:def 1;
then A5: A1 c= (Cl A2) ` by SUBSET_1:23;
A6: A2 c= Cl A2 by PRE_TOPC:18;
A7: (A1 \/ A2) /\ ((Cl A2) `) = (A1 \/ A2) \ (Cl A2) by SUBSET_1:13
.= (A1 \ (Cl A2)) \/ (A2 \ (Cl A2)) by XBOOLE_1:42
.= (A1 \ (Cl A2)) \/ {} by A6, XBOOLE_1:37
.= A1 /\ ((Cl A2) `) by SUBSET_1:13
.= A1 by A5, XBOOLE_1:28 ;
(A1 \/ A2) /\ ((Cl A1) `) = (A1 \/ A2) \ (Cl A1) by SUBSET_1:13
.= (A1 \ (Cl A1)) \/ (A2 \ (Cl A1)) by XBOOLE_1:42
.= {} \/ (A2 \ (Cl A1)) by A2, XBOOLE_1:37
.= A2 /\ ((Cl A1) `) by SUBSET_1:13
.= A2 by A4, XBOOLE_1:28 ;
hence ( A1 is open & A2 is open ) by A1, A7; :: thesis: verum