let C be non empty set ; :: thesis: for f, g, h being Membership_Func of C st max g,h c= & min f,h = EMF C holds
g c=
let f, g, h be Membership_Func of C; :: thesis: ( max g,h c= & min f,h = EMF C implies g c= )
assume A1: ( max g,h c= & min f,h = EMF C ) ; :: thesis: g c=
then min f,(max g,h) = f by Th30;
then A2: f = max (min f,g),(min f,h) by Th10
.= min f,g by A1, Th19 ;
let x be Element of C; :: according to FUZZY_1:def 3 :: thesis: f . x <= g . x
f . x = min (f . x),(g . x) by A2, Def4;
hence f . x <= g . x by XXREAL_0:def 9; :: thesis: verum