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 3 :: 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 Def5;
hence (min f,g) . x <= (max f,g) . x by Def4; :: thesis: verum