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 3 :: thesis: (f * g) . c <= (min f,g) . c
A1: (min f,g) . c = min (f . c),(g . c) by FUZZY_1:6;

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

(f * g) . c <= (min f,g) . c

proof

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

end;

hence (f * g) . c <= (min f,g) . c ; :: thesis: verum

end;

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

(f * g) . c <= (min f,g) . c

proof

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

end;

hence (f * g) . c <= (min f,g) . c ; :: thesis: verum

end;

end;