let C be non empty set ; :: thesis: for f, g, h being Membership_Func of C st max ((min (f,g)),(min (f,h))) = f holds
max (g,h) c=
let f, g, h be Membership_Func of C; :: thesis: ( max ((min (f,g)),(min (f,h))) = f implies max (g,h) c= )
assume A1: max ((min (f,g)),(min (f,h))) = f ; :: thesis: max (g,h) c=
let x be Element of C; :: according to FUZZY_1:def 3 :: thesis: f . x <= (max (g,h)) . x
(max ((min (f,g)),(min (f,h)))) . x = max (((min (f,g)) . x),((min (f,h)) . x)) by Def5
.= max (((min (f,g)) . x),(min ((f . x),(h . x)))) by Def4
.= max ((min ((f . x),(g . x))),(min ((f . x),(h . x)))) by Def4
.= 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 Def5; :: thesis: verum