let C be non empty set ; for f, h, g being Membership_Func of C st g c= holds
max (g,h) c=
let f, h, g be Membership_Func of C; ( g c= implies max (g,h) c= )
assume A1:
g c=
; max (g,h) c=
let x be Element of C; FUZZY_1:def 2 (max (f,h)) . x <= (max (g,h)) . x
f . x <= g . x
by A1;
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 Def4;
hence
(max (f,h)) . x <= (max (g,h)) . x
by Def4; verum