let C be non empty set ; for f, h, g, h1 being Membership_Func of C st g c= & h1 c= holds
g \ h c=
let f, h, g, h1 be Membership_Func of C; ( g c= & h1 c= implies g \ h c= )
assume that
A1:
for c being Element of C holds f . c <= g . c
and
A2:
for c being Element of C holds h . c <= h1 . c
; FUZZY_1:def 2 g \ h c=
let c be Element of C; FUZZY_1:def 2 (f \ h1) . c <= (g \ h) . c
h . c <= h1 . c
by A2;
then A3:
1 - (h . c) >= 1 - (h1 . c)
by XREAL_1:10;
f . c <= g . c
by A1;
then
min ((f . c),(1 - (h1 . c))) <= min ((g . c),(1 - (h . c)))
by A3, XXREAL_0:18;
then
min ((f . c),((1_minus h1) . c)) <= min ((g . c),(1 - (h . c)))
by FUZZY_1:def 5;
then
min ((f . c),((1_minus h1) . c)) <= min ((g . c),((1_minus h) . c))
by FUZZY_1:def 5;
then
(min (f,(1_minus h1))) . c <= min ((g . c),((1_minus h) . c))
by FUZZY_1:5;
hence
(f \ h1) . c <= (g \ h) . c
by FUZZY_1:5; verum