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

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

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

proof

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

end;

end;

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