let GX be non empty TopSpace; 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; ( 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 = {}
; XBOOLE_0:def 7 A misses Component_of B
A4:
A is connected
by A1;
assume
A /\ (Component_of B) <> {}
; XBOOLE_0:def 7 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; verum