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