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

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