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 )

proof

let Y be Subset of V; :: thesis: ( Y in SF iff Y in SG )

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

assume 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;

assume Y in SG ; :: thesis: Y in SF
then ( Y is convex & M c= Y ) by A2;
hence Y in SF by A1; :: thesis: verum

end;

hence SF = SG by SETFAM_1:31; :: thesis: verum