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 <> {} 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; :: thesis: verum

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 <> {} 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; :: thesis: verum