let C be non empty set ; :: thesis: for f, g being Membership_Func of C st g c= holds

g c=

let f, g be Membership_Func of C; :: thesis: ( g c= implies g c= )

assume A1: for c being Element of C holds f . c <= g . c ; :: according to FUZZY_1:def 2 :: thesis: g c=

let c be Element of C; :: according to FUZZY_1:def 2 :: thesis: (max (f,(g \ f))) . c <= g . c

A2: f . c <= g . c by A1;

(max (f,(g \ f))) . c = (min ((max (f,g)),(max (f,(1_minus f))))) . c by FUZZY_1:9

.= min (((max (f,g)) . c),((max (f,(1_minus f))) . c)) by FUZZY_1:5

.= min ((max ((f . c),(g . c))),((max (f,(1_minus f))) . c)) by FUZZY_1:5

.= min ((g . c),((max (f,(1_minus f))) . c)) by A2, XXREAL_0:def 10 ;

hence (max (f,(g \ f))) . c <= g . c by XXREAL_0:17; :: thesis: verum

g c=

let f, g be Membership_Func of C; :: thesis: ( g c= implies g c= )

assume A1: for c being Element of C holds f . c <= g . c ; :: according to FUZZY_1:def 2 :: thesis: g c=

let c be Element of C; :: according to FUZZY_1:def 2 :: thesis: (max (f,(g \ f))) . c <= g . c

A2: f . c <= g . c by A1;

(max (f,(g \ f))) . c = (min ((max (f,g)),(max (f,(1_minus f))))) . c by FUZZY_1:9

.= min (((max (f,g)) . c),((max (f,(1_minus f))) . c)) by FUZZY_1:5

.= min ((max ((f . c),(g . c))),((max (f,(1_minus f))) . c)) by FUZZY_1:5

.= min ((g . c),((max (f,(1_minus f))) . c)) by A2, XXREAL_0:def 10 ;

hence (max (f,(g \ f))) . c <= g . c by XXREAL_0:17; :: thesis: verum