let GX be non empty TopSpace; :: thesis: for A, B being Subset of GX st A is a_component & B is connected & B <> {} & A misses B holds
A misses Component_of B
let A, B be Subset of GX; :: thesis: ( A is a_component & B is connected & B <> {} & A misses B implies A misses Component_of B )
assume that
A1: A is a_component and
A2: ( B is connected & B <> {} ) and
A3: A /\ B = {} ; :: according to XBOOLE_0:def 7 :: thesis: A misses Component_of B
A4: A is connected by A1;
assume A /\ (Component_of B) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider x being Point of GX such that
A5: x in A /\ (Component_of B) by SUBSET_1:4;
x in A by A5, XBOOLE_0:def 4;
then A6: Component_of x = Component_of A by A4, Th15;
A7: x in Component_of B by A5, XBOOLE_0:def 4;
( Component_of A = A & Component_of B = Component_of (Component_of B) ) by A1, A2, Th7, Th11;
then (Component_of B) /\ B = {} by A2, A3, A7, A6, Th5, Th15;
hence contradiction by A2, Th1, XBOOLE_1:28; :: thesis: verum