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