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