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 that
A1: ( B1 is open & B2 is open & B1 meets A ) and
A2: B2 meets A and
A3: A c= B1 \/ B2 and
A4: B1 misses B2 ; :: thesis: not A is connected
reconsider C1 = B1 /\ A, C2 = B2 /\ A as Subset of X ;
A5: A = (B1 \/ B2) /\ A by A3, XBOOLE_1:28
.= C1 \/ C2 by XBOOLE_1:23 ;
A6: C2 <> {} by A2, XBOOLE_0:def 7;
A7: ( 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:15;
A8: ( C1 c= B1 & C2 c= B2 ) by XBOOLE_1:17;
( B1,B2 are_separated & C1 <> {} ) by A1, A4, TSEP_1:37, XBOOLE_0:def 7;
hence not A is connected by A7, A5, A8, A6, CONNSP_1:7; :: thesis: verum