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;

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

suppose A2: (min (f,g)) . c = f . c ; :: thesis: (f * g) . c <= (min (f,g)) . c

A3: f . c >= 0 by Th1;
g . c <= 1 by Th1;
then (g . c) * (f . c) <= 1 * (f . c) by A3, XREAL_1:64;
hence (f * g) . c <= (min (f,g)) . c by A2, Def2; :: thesis: verum

end;

suppose A4: (min (f,g)) . c = g . c ; :: thesis: (f * g) . c <= (min (f,g)) . c

A5: g . c >= 0 by Th1;
f . c <= 1 by Th1;
then (f . c) * (g . c) <= 1 * (g . c) by A5, XREAL_1:64;
hence (f * g) . c <= (min (f,g)) . c by A4, Def2; :: thesis: verum

end;

end;