let C be non empty set ; :: thesis:
let f, g, h be Membership_Func of C; :: thesis:

hereby :: thesis:

assume A1: f = max g,h ; :: thesis:
hence ( f c= & f c= ) by Th18; :: thesis:
let h1 be Membership_Func of C; :: thesis:
assume A2: ( h1 c= & h1 c= ) ; :: thesis:
thus h1 c= :: thesis:

proof

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

end;

end;

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