let C be non empty set ; :: thesis: for f, g being Membership_Func of C holds
( f c= & max (f,g) c= )
let f, g be Membership_Func of C; :: thesis: ( f c= & max (f,g) c= )
thus f c= :: thesis: max (f,g) c=

proof

let x be Element of C; :: according to FUZZY_1:def 2 :: thesis: (min (f,g)) . x <= f . x
(min (f,g)) . x = min ((f . x),(g . x)) by Def3;
hence (min (f,g)) . x <= f . x by XXREAL_0:17; :: thesis: verum

end;

let x be Element of C; :: according to FUZZY_1:def 2 :: thesis: f . x <= (max (f,g)) . x
(max (f,g)) . x = max ((f . x),(g . x)) by Def4;
hence f . x <= (max (f,g)) . x by XXREAL_0:25; :: thesis: verum