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