let S, S9 be Subset of GX; :: thesis: ( ex F being Subset-Family of GX st
( ( for A being Subset of GX holds
( A in F iff ( A is connected & x in A ) ) ) & union F = S ) & ex F being Subset-Family of GX st
( ( for A being Subset of GX holds
( A in F iff ( A is connected & x in A ) ) ) & union F = S9 ) implies S = S9 )

assume that
A2: ex F being Subset-Family of GX st
( ( for A being Subset of GX holds
( A in F iff ( A is connected & x in A ) ) ) & union F = S ) and
A3: ex F9 being Subset-Family of GX st
( ( for A being Subset of GX holds
( A in F9 iff ( A is connected & x in A ) ) ) & union F9 = S9 ) ; :: thesis: S = S9
consider F being Subset-Family of GX such that
A4: for A being Subset of GX holds
( A in F iff ( A is connected & x in A ) ) and
A5: union F = S by A2;
consider F9 being Subset-Family of GX such that
A6: for A being Subset of GX holds
( A in F9 iff ( A is connected & x in A ) ) and
A7: union F9 = S9 by A3;
now :: thesis: for y being object holds
( y in S iff y in S9 )
let y be object ; :: thesis: ( y in S iff y in S9 )
A8: now :: thesis: ( y in S9 implies y in S )
assume y in S9 ; :: thesis: y in S
then consider B being set such that
A9: y in B and
A10: B in F9 by ;
reconsider B = B as Subset of GX by A10;
A11: x in B by ;
B is connected by ;
then B in F by ;
hence y in S by ; :: thesis: verum
end;
now :: thesis: ( y in S implies y in S9 )
assume y in S ; :: thesis: y in S9
then consider B being set such that
A12: y in B and
A13: B in F by ;
reconsider B = B as Subset of GX by A13;
A14: x in B by ;
B is connected by ;
then B in F9 by ;
hence y in S9 by ; :: thesis: verum
end;
hence ( y in S iff y in S9 ) by A8; :: thesis: verum
end;
hence S = S9 by TARSKI:2; :: thesis: verum