let C be non empty set ; :: thesis: for f, g, h being Membership_Func of C holds
( f = min g,h iff ( g c= & h c= & ( for h1 being Membership_Func of C st g c= & h c= holds
f c= ) ) )
let f, g, h be Membership_Func of C; :: thesis: ( f = min g,h iff ( g c= & h c= & ( for h1 being Membership_Func of C st g c= & h c= holds
f c= ) ) )

hereby :: thesis: ( g c= & h c= & ( for h1 being Membership_Func of C st g c= & h c= holds
f c= ) implies f = min g,h )

assume A1: f = min g,h ; :: thesis: ( g c= & h c= & ( for h1 being Membership_Func of C st g c= & h c= holds
f c= ) )
hence ( g c= & h c= ) by Th18; :: thesis: for h1 being Membership_Func of C st g c= & h c= holds
f c=
let h1 be Membership_Func of C; :: thesis: ( g c= & h c= implies f c= )
assume A2: ( g c= & h c= ) ; :: thesis: f c=
thus f c= :: thesis: verum

proof

let x be Element of C; :: according to FUZZY_1:def 3 :: thesis: h1 . x <= f . x
( h1 . x <= g . x & h1 . x <= h . x ) by A2, Def3;
then min (g . x),(h . x) >= h1 . x by XXREAL_0:20;
hence h1 . x <= f . x by A1, Def4; :: thesis: verum

end;

end;

assume that
A3: g c= and
A4: h c= and
A5: for h1 being Membership_Func of C st g c= & h c= holds
f c= ; :: thesis: f = min g,h
A6: min g,h c= by A3, A4, Th25;
( g c= & h c= ) by Th18;
then f c= by A5;
hence f = min g,h by A6, Lm1; :: thesis: verum