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