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