let X be non empty set ; :: thesis: for f, g being Membership_Func of X holds max (f,g) c=
let f, g be Membership_Func of X; :: thesis: max (f,g) c=
let x be Element of X; :: according to FUZZY_1:def 2 :: thesis: f . x <= (max (f,g)) . x
(max (f,g)) . x = max ((f . x),(g . x)) by FUZZY_1:def 4;
hence f . x <= (max (f,g)) . x by XXREAL_0:25; :: thesis: verum