let C be non empty set ; :: thesis: for f, g, h being Membership_Func of C holds (min f,g) \ (min f,h) c=
let f, g, h be Membership_Func of C; :: thesis: (min f,g) \ (min f,h) c=
let c be Element of C; :: according to FUZZY_1:def 3 :: thesis: (min f,(g \ h)) . c <= ((min f,g) \ (min f,h)) . c
(1_minus h) . c <= max ((1_minus f) . c),((1_minus h) . c) by XXREAL_0:25;
then min ((min f,g) . c),((1_minus h) . c) <= min ((min f,g) . c),(max ((1_minus f) . c),((1_minus h) . c)) by XXREAL_0:18;
then min ((min f,g) . c),((1_minus h) . c) <= min ((min f,g) . c),((max (1_minus f),(1_minus h)) . c) by FUZZY_1:6;
then A1: min ((min f,g) . c),((1_minus h) . c) <= (min (min f,g),(max (1_minus f),(1_minus h))) . c by FUZZY_1:6;
(min f,(g \ h)) . c = (min (min f,g),(1_minus h)) . c by FUZZY_1:8
.= min ((min f,g) . c),((1_minus h) . c) by FUZZY_1:6 ;
hence (min f,(g \ h)) . c <= ((min f,g) \ (min f,h)) . c by A1, FUZZY_1:12; :: thesis: verum