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 that
A1: max g,h c= and
A2: min f,h = EMF C ; :: thesis: g c=
let x be Element of C; :: according to FUZZY_1:def 3 :: thesis: f . x <= g . x
min f,(max g,h) = f by A1, Th30;
then f = max (min f,g),(min f,h) by Th10
.= min f,g by A2, Th19 ;
then f . x = min (f . x),(g . x) by Def4;
hence f . x <= g . x by XXREAL_0:def 9; :: thesis: verum