let GX be non empty TopSpace; for A, B, C, D being Subset of GX st B is connected & C is_a_component_of D & A c= C & A meets B & B c= D holds
B c= C
let A, B, C, D be Subset of GX; ( B is connected & C is_a_component_of D & A c= C & A meets B & B c= D implies B c= C )
assume that
A1:
B is connected
and
A2:
C is_a_component_of D
and
A3:
A c= C
and
A4:
A meets B
and
A5:
B c= D
; B c= C
A6:
A <> {}
by A4;
A7:
B <> {}
by A4;
reconsider A = A, B = B as non empty Subset of GX by A4;
reconsider C = C, D = D as non empty Subset of GX by A3, A5, A6, A7, XBOOLE_1:3;
consider CC being Subset of GX such that
A8:
CC is_a_component_of D
and
A9:
B c= CC
by A1, A5, Th3;
A10:
A meets CC
by A4, A9, XBOOLE_1:63;
A11:
ex C1 being Subset of (GX | D) st
( C1 = C & C1 is a_component )
by A2, CONNSP_1:def 6;
ex CC1 being Subset of (GX | D) st
( CC1 = CC & CC1 is a_component )
by A8, CONNSP_1:def 6;
hence
B c= C
by A3, A9, A10, A11, CONNSP_1:35, XBOOLE_1:63; verum