let C be non empty set ; :: thesis: 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; :: 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 2 :: 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 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; :: thesis: verum