let S, S' be Subset of ; :: thesis: ( ex F being Subset-Family of st
( ( for A being Subset of holds
( A in F iff ( A is connected & V c= A ) ) ) & union F = S ) & ex F being Subset-Family of st
( ( for A being Subset of holds
( A in F iff ( A is connected & V c= A ) ) ) & union F = S' ) implies S = S' )
assume that
A2: ex F being Subset-Family of st
( ( for A being Subset of holds
( A in F iff ( A is connected & V c= A ) ) ) & union F = S ) and
A3: ex F' being Subset-Family of st
( ( for A being Subset of holds
( A in F' iff ( A is connected & V c= A ) ) ) & union F' = S' ) ; :: thesis: S = S'
consider F being Subset-Family of such that
A4: for A being Subset of holds
( A in F iff ( A is connected & V c= A ) ) and
A5: union F = S by A2;
consider F' being Subset-Family of such that
A6: for A being Subset of holds
( A in F' iff ( A is connected & V c= A ) ) and
A7: union F' = S' by A3;

now

let y be set ; :: thesis: ( y in S iff y in S' )

A8: now

assume y in S' ; :: thesis: y in S
then consider B being set such that
A9: y in B and
A10: B in F' by A7, TARSKI:def 4;
reconsider B = B as Subset of by A10;
( B is connected & V c= B ) by A6, A10;
then B in F by A4;
hence y in S by A5, A9, TARSKI:def 4; :: thesis: verum

end;

now

assume y in S ; :: thesis: y in S'
then consider B being set such that
A11: y in B and
A12: B in F by A5, TARSKI:def 4;
reconsider B = B as Subset of by A12;
( B is connected & V c= B ) by A4, A12;
then B in F' by A6;
hence y in S' by A7, A11, TARSKI:def 4; :: thesis: verum

end;

hence ( y in S iff y in S' ) by A8; :: thesis: verum

end;

hence S = S' by TARSKI:2; :: thesis: verum