let SF, SG be Subset-Family of V; :: thesis: ( ( for N being Subset of V holds

( N in SF iff ( N is convex & M c= N ) ) ) & ( for N being Subset of V holds

( N in SG iff ( N is convex & M c= N ) ) ) implies SF = SG )

assume that

A1: for N being Subset of V holds

( N in SF iff ( N is convex & M c= N ) ) and

A2: for N being Subset of V holds

( N in SG iff ( N is convex & M c= N ) ) ; :: thesis: SF = SG

for Y being Subset of V holds

( Y in SF iff Y in SG )

( N in SF iff ( N is convex & M c= N ) ) ) & ( for N being Subset of V holds

( N in SG iff ( N is convex & M c= N ) ) ) implies SF = SG )

assume that

A1: for N being Subset of V holds

( N in SF iff ( N is convex & M c= N ) ) and

A2: for N being Subset of V holds

( N in SG iff ( N is convex & M c= N ) ) ; :: thesis: SF = SG

for Y being Subset of V holds

( Y in SF iff Y in SG )

proof

hence
SF = SG
by SETFAM_1:31; :: thesis: verum
let Y be Subset of V; :: thesis: ( Y in SF iff Y in SG )

then ( Y is convex & M c= Y ) by A2;

hence Y in SF by A1; :: thesis: verum

end;hereby :: thesis: ( Y in SG implies Y in SF )

assume
Y in SG
; :: thesis: Y in SFassume
Y in SF
; :: thesis: Y in SG

then ( Y is convex & M c= Y ) by A1;

hence Y in SG by A2; :: thesis: verum

end;then ( Y is convex & M c= Y ) by A1;

hence Y in SG by A2; :: thesis: verum

then ( Y is convex & M c= Y ) by A2;

hence Y in SF by A1; :: thesis: verum