let C be non empty set ; :: thesis: 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; :: thesis: (min (f,g)) \ (min (f,h)) c=

let c be Element of C; :: according to FUZZY_1:def 2 :: 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: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; :: thesis: verum

let f, h, g be Membership_Func of C; :: thesis: (min (f,g)) \ (min (f,h)) c=

let c be Element of C; :: according to FUZZY_1:def 2 :: 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: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; :: thesis: verum