let C be non empty set ; for f, g being Membership_Func of C st g c= holds
g c=
let f, g be Membership_Func of C; ( g c= implies g c= )
assume A1:
for c being Element of C holds f . c <= g . c
; FUZZY_1:def 3 g c=
let c be Element of C; FUZZY_1:def 3 (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; verum