let C be non empty set ; for f, h, g being Membership_Func of C holds (min (f,g)) \ (min (f,h)) c=
let f, h, g be Membership_Func of C; (min (f,g)) \ (min (f,h)) c=
let c be Element of C; FUZZY_1:def 2 (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:5;
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:5;
(min (f,(g \ h))) . c =
(min ((min (f,g)),(1_minus h))) . c
by FUZZY_1:7
.=
min (((min (f,g)) . c),((1_minus h) . c))
by FUZZY_1:5
;
hence
(min (f,(g \ h))) . c <= ((min (f,g)) \ (min (f,h))) . c
by A1, FUZZY_1:11; verum