let C be non empty set ; :: thesis: for f, h, g 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, h, g 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 Th16; :: 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 2 :: thesis: h1 . x <= f . x
( h1 . x <= g . x & h1 . x <= h . x ) by A2;
then min ((g . x),(h . x)) >= h1 . x by XXREAL_0:20;
hence h1 . x <= f . x by A1, Def3; :: thesis: verum
end;
end;
assume that
A3: ( g c= & h c= ) and
A4: for h1 being Membership_Func of C st g c= & h c= holds
f c= ; :: thesis: f = min (g,h)
( g c= & h c= ) by Th16;
then A5: f c= by A4;
min (g,h) c= by A3, Th23;
hence f = min (g,h) by A5, Lm1; :: thesis: verum