let GX be non empty TopSpace; :: thesis: for A, V being Subset of GX st A is a_component & V is connected & V c= A & V <> {} holds

A = Component_of V

let A, V be Subset of GX; :: thesis: ( A is a_component & V is connected & V c= A & V <> {} implies A = Component_of V )

assume that

A1: A is a_component and

A2: V is connected and

A3: V c= A and

A4: V <> {} ; :: thesis: A = Component_of V

V c= Component_of V by A2, Th1;

then A5: A meets Component_of V by A3, A4, XBOOLE_1:67;

assume A6: A <> Component_of V ; :: thesis: contradiction

Component_of V is a_component by A2, A4, Th8;

hence contradiction by A1, A6, A5, CONNSP_1:1, CONNSP_1:34; :: thesis: verum

A = Component_of V

let A, V be Subset of GX; :: thesis: ( A is a_component & V is connected & V c= A & V <> {} implies A = Component_of V )

assume that

A1: A is a_component and

A2: V is connected and

A3: V c= A and

A4: V <> {} ; :: thesis: A = Component_of V

V c= Component_of V by A2, Th1;

then A5: A meets Component_of V by A3, A4, XBOOLE_1:67;

assume A6: A <> Component_of V ; :: thesis: contradiction

Component_of V is a_component by A2, A4, Th8;

hence contradiction by A1, A6, A5, CONNSP_1:1, CONNSP_1:34; :: thesis: verum