let C be non empty set ; :: thesis: for f, g, h being Membership_Func of C holds min f,(g * h) c=
let f, g, h be Membership_Func of C; :: thesis: min f,(g * h) c=
let c be Element of C; :: according to FUZZY_1:def 3 :: thesis: ((min f,g) * (min f,h)) . c <= (min f,(g * h)) . c
A1: ((min f,g) * (min f,h)) . c = ((min f,g) . c) * ((min f,h) . c) by Def2
.= (min (f . c),(g . c)) * ((min f,h) . c) by FUZZY_1:6
.= (min (f . c),(g . c)) * (min (f . c),(h . c)) by FUZZY_1:6 ;
(min (f . c),(g . c)) * (min (f . c),(h . c)) <= (min f,(g * h)) . c

proof

now

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

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

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

proof

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

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

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

proof

A4: ( f . c <= g . c & f . c <= h . c ) by A2, A3, XXREAL_0:def 9;
( 0 <= g . c & 0 <= f . c ) by Th1;
then ( (f . c) * (f . c) <= (g . c) * (f . c) & (g . c) * (f . c) <= (h . c) * (g . c) ) by A4, XREAL_1:66;
then A5: (f . c) * (f . c) <= (g . c) * (h . c) by XXREAL_0:2;
f c= by Th33;
then (f * f) . c <= f . c by FUZZY_1:def 3;
then min ((f * f) . c),((f . c) * (f . c)) <= min (f . c),((g . c) * (h . c)) by A5, XXREAL_0:18;
then min ((f . c) * (f . c)),((f . c) * (f . c)) <= min (f . c),((g . c) * (h . c)) by Def2;
then (f . c) * (f . c) <= min (f . c),((g * h) . c) by Def2;
hence (min (f . c),(g . c)) * (min (f . c),(h . c)) <= (min f,(g * h)) . c by A2, A3, FUZZY_1:6; :: thesis: verum

end;

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

end;

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

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

proof

( f . c >= 0 & 1 >= h . c & f . c <= g . c & h . c >= 0 ) by A2, Th1, XXREAL_0:def 9;
then ( (f . c) * (h . c) <= (f . c) * 1 & (f . c) * (h . c) <= (g . c) * (h . c) ) by XREAL_1:66;
then (f . c) * (h . c) <= min (f . c),((g . c) * (h . c)) by XXREAL_0:20;
then (f . c) * (h . c) <= min (f . c),((g * h) . c) by Def2;
hence (min (f . c),(g . c)) * (min (f . c),(h . c)) <= (min f,(g * h)) . c by A2, A6, FUZZY_1:6; :: thesis: verum

end;

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

end;

end;

end;

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

end;

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

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

proof

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

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

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

proof

( f . c >= 0 & 1 >= g . c & f . c <= h . c & g . c >= 0 ) by A8, Th1, XXREAL_0:def 9;
then ( (g . c) * (f . c) <= (f . c) * 1 & (f . c) * (g . c) <= (h . c) * (g . c) ) by XREAL_1:66;
then (f . c) * (g . c) <= min (f . c),((h . c) * (g . c)) by XXREAL_0:20;
then (f . c) * (g . c) <= min (f . c),((g * h) . c) by Def2;
hence (min (f . c),(g . c)) * (min (f . c),(h . c)) <= (min f,(g * h)) . c by A7, A8, FUZZY_1:6; :: thesis: verum

end;

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

end;

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

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

proof

f c= by Th33;
then ( g . c >= 0 & h . c <= f . c & f . c >= 0 & g . c <= f . c & (f * f) . c <= f . c ) by A7, A9, Th1, FUZZY_1:def 3, XXREAL_0:def 9;
then ( (h . c) * (g . c) <= (f . c) * (g . c) & (g . c) * (f . c) <= (f . c) * (f . c) & (f . c) * (f . c) <= f . c ) by Def2, XREAL_1:66;
then ( (h . c) * (g . c) <= (f . c) * (f . c) & (f . c) * (f . c) <= f . c ) by XXREAL_0:2;
then (h . c) * (g . c) <= f . c by XXREAL_0:2;
then (h . c) * (g . c) <= min (f . c),((h . c) * (g . c)) by XXREAL_0:20;
then (g . c) * (h . c) <= min (f . c),((g * h) . c) by Def2;
hence (min (f . c),(g . c)) * (min (f . c),(h . c)) <= (min f,(g * h)) . c by A7, A9, FUZZY_1:6; :: thesis: verum

end;

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

end;

end;

end;

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

end;

end;

end;

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

end;

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