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

let f, g be Membership_Func of C; :: thesis: min (f,g) c=

let c be Element of C; :: according to FUZZY_1:def 2 :: thesis: (f * g) . c <= (min (f,g)) . c

A1: (min (f,g)) . c = min ((f . c),(g . c)) by FUZZY_1:5;

let f, g be Membership_Func of C; :: thesis: min (f,g) c=

let c be Element of C; :: according to FUZZY_1:def 2 :: thesis: (f * g) . c <= (min (f,g)) . c

A1: (min (f,g)) . c = min ((f . c),(g . c)) by FUZZY_1:5;

per cases
( (min (f,g)) . c = f . c or (min (f,g)) . c = g . c )
by A1, XXREAL_0:15;

end;