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 3 :: thesis: g c=
let c be Element of C; :: according to FUZZY_1:def 3 :: 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:10
.= min ((max f,g) . c),((max f,(1_minus f)) . c) by FUZZY_1:6
.= min (max (f . c),(g . c)),((max f,(1_minus f)) . c) by FUZZY_1:6
.= 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