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 3 :: thesis: (max f,g) . x <= h . x
A2: ( f . x <= h . x & g . x <= h . x ) by A1, Def3;
max (f . x),(g . x) = (max f,g) . x by Def5;
hence (max f,g) . x <= h . x by A2, XXREAL_0:28; :: thesis: verum