let C be non empty set ; for f, h, g being Membership_Func of C st max ((min (f,g)),(min (f,h))) = f holds
max (g,h) c=
let f, h, g be Membership_Func of C; ( max ((min (f,g)),(min (f,h))) = f implies max (g,h) c= )
assume A1:
max ((min (f,g)),(min (f,h))) = f
; max (g,h) c=
let x be Element of C; FUZZY_1:def 2 f . x <= (max (g,h)) . x
(max ((min (f,g)),(min (f,h)))) . x =
max (((min (f,g)) . x),((min (f,h)) . x))
by Def4
.=
max (((min (f,g)) . x),(min ((f . x),(h . x))))
by Def3
.=
max ((min ((f . x),(g . x))),(min ((f . x),(h . x))))
by Def3
.=
min ((f . x),(max ((g . x),(h . x))))
by XXREAL_0:38
;
then
f . x <= max ((g . x),(h . x))
by A1, XXREAL_0:def 9;
hence
f . x <= (max (g,h)) . x
by Def4; verum