let GX be non empty TopSpace; :: thesis: 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; :: thesis: ( 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
; :: thesis: B c= C
A6:
( A <> {} & B <> {} )
by A4, XBOOLE_1:65;
reconsider A = A, B = B as non empty Subset of GX by A4, XBOOLE_1:65;
reconsider C = C, D = D as non empty Subset of GX by A3, A5, A6, XBOOLE_1:3;
consider CC being Subset of GX such that
A7:
CC is_a_component_of D
and
A8:
B c= CC
by A1, A5, Th5;
A9:
A meets CC
by A4, A8, XBOOLE_1:63;
consider C1 being Subset of (GX | D) such that
A10:
C1 = C
and
A11:
C1 is_a_component_of GX | D
by A2, CONNSP_1:def 6;
consider CC1 being Subset of (GX | D) such that
A12:
CC1 = CC
and
A13:
CC1 is_a_component_of GX | D
by A7, CONNSP_1:def 6;
thus
B c= C
by A3, A8, A9, A10, A11, A12, A13, CONNSP_1:37, XBOOLE_1:63; :: thesis: verum