let C be non empty set ; :: thesis: for f, g being Membership_Func of C holds max (f,g) c=
let f, g be Membership_Func of C; :: thesis: max (f,g) c=
let x be Element of C; :: according to FUZZY_1:def 2 :: thesis: (min (f,g)) . x <= (max (f,g)) . x
( min ((f . x),(g . x)) <= f . x & f . x <= max ((f . x),(g . x)) ) by XXREAL_0:17, XXREAL_0:25;
then min ((f . x),(g . x)) <= max ((f . x),(g . x)) by XXREAL_0:2;
then min ((f . x),(g . x)) <= (max (f,g)) . x by Def4;
hence (min (f,g)) . x <= (max (f,g)) . x by Def3; :: thesis: verum