let C be non empty set ; :: thesis: for f, g, h being Membership_Func of C st g c= holds
max g,h c=
let f, g, h be Membership_Func of C; :: thesis: ( g c= implies max g,h c= )
assume A1: g c= ; :: thesis: max g,h c=
let x be Element of C; :: according to FUZZY_1:def 3 :: thesis: (max f,h) . x <= (max g,h) . x
f . x <= g . x by A1, Def3;
then max (f . x),(h . x) <= max (g . x),(h . x) by XXREAL_0:26;
then max (f . x),(h . x) <= (max g,h) . x by Def5;
hence (max f,h) . x <= (max g,h) . x by Def5; :: thesis: verum