let X be non empty TopSpace; :: thesis: for A, B1, B2 being Subset of X st B1 is open & B2 is open & B1 meets A & B2 meets A & A c= B1 \/ B2 & B1 misses B2 holds
not A is connected
let A, B1, B2 be Subset of X; :: thesis: ( B1 is open & B2 is open & B1 meets A & B2 meets A & A c= B1 \/ B2 & B1 misses B2 implies not A is connected )
assume A1: ( B1 is open & B2 is open & B1 meets A & B2 meets A & A c= B1 \/ B2 & B1 misses B2 ) ; :: thesis: not A is connected
A2: ( A is connected iff for P, Q being Subset of X st A = P \/ Q & P,Q are_separated & not P = {} X holds
Q = {} X ) by CONNSP_1:16;
reconsider C1 = B1 /\ A, C2 = B2 /\ A as Subset of X ;
A3: B1,B2 are_separated by A1, TSEP_1:41;
A4: A = (B1 \/ B2) /\ A by A1, XBOOLE_1:28
.= C1 \/ C2 by XBOOLE_1:23 ;
A5: ( C1 c= B1 & C2 c= B2 ) by XBOOLE_1:17;
( C1 <> {} & C2 <> {} ) by A1, XBOOLE_0:def 7;
hence not A is connected by A2, A3, A4, A5, CONNSP_1:8; :: thesis: verum