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;

( ( 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 )

hence
S = S9
by TARSKI:2; :: thesis: verum( y in S iff y in S9 )

let y be object ; :: thesis: ( y in S iff y in S9 )

end;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 A7, TARSKI:def 4;

reconsider B = B as Subset of GX by A10;

A11: x in B by A6, A10;

B is connected by A6, A10;

then B in F by A4, A11;

hence y in S by A5, A9, TARSKI:def 4; :: thesis: verum

end;then consider B being set such that

A9: y in B and

A10: B in F9 by A7, TARSKI:def 4;

reconsider B = B as Subset of GX by A10;

A11: x in B by A6, A10;

B is connected by A6, A10;

then B in F by A4, A11;

hence y in S by A5, A9, TARSKI:def 4; :: thesis: verum

now :: thesis: ( y in S implies y in S9 )

hence
( y in S iff y in S9 )
by A8; :: thesis: verumassume
y in S
; :: thesis: y in S9

then consider B being set such that

A12: y in B and

A13: B in F by A5, TARSKI:def 4;

reconsider B = B as Subset of GX by A13;

A14: x in B by A4, A13;

B is connected by A4, A13;

then B in F9 by A6, A14;

hence y in S9 by A7, A12, TARSKI:def 4; :: thesis: verum

end;then consider B being set such that

A12: y in B and

A13: B in F by A5, TARSKI:def 4;

reconsider B = B as Subset of GX by A13;

A14: x in B by A4, A13;

B is connected by A4, A13;

then B in F9 by A6, A14;

hence y in S9 by A7, A12, TARSKI:def 4; :: thesis: verum