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

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