let GX be non empty TopSpace; :: thesis: for A being Subset of GX holds
( A is a_component iff ex V being Subset of GX st
( V is connected & V <> {} & A = Component_of V ) )
let A be Subset of GX; :: thesis: ( A is a_component iff ex V being Subset of GX st
( V is connected & V <> {} & A = Component_of V ) )
A1: now :: thesis: ( A is a_component implies ex V being Subset of GX st
( V is connected & V <> {} & A = Component_of V ) )
assume A2: A is a_component ; :: thesis: ex V being Subset of GX st
( V is connected & V <> {} & A = Component_of V )
take V = A; :: thesis: ( V is connected & V <> {} & A = Component_of V )
thus ( V is connected & V <> {} & A = Component_of V ) by A2, Th7; :: thesis: verum
end;
now :: thesis: ( ex V being Subset of GX st
( V is connected & V <> {} & A = Component_of V ) implies A is a_component )
given V being Subset of GX such that A3: ( V is connected & V <> {} & A = Component_of V ) ; :: thesis: A is a_component
( A is connected & ( for B being Subset of GX st B is connected & A c= B holds
A = B ) ) by A3, Th5, Th6;
hence A is a_component by CONNSP_1:def 5; :: thesis: verum
end;
hence ( A is a_component iff ex V being Subset of GX st
( V is connected & V <> {} & A = Component_of V ) ) by A1; :: thesis: verum