let C be non empty set ; :: thesis: for f, h, g being Membership_Func of C st max (g,h) c= & min (f,h) = EMF C holds
g c=
let f, h, g 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 2 :: thesis: f . x <= g . x
min (f,(max (g,h))) = f by A1, Th26;
then f = max ((min (f,g)),(min (f,h))) by Th9
.= min (f,g) by A2, Th17 ;
then f . x = min ((f . x),(g . x)) by Def3;
hence f . x <= g . x by XXREAL_0:def 9; :: thesis: verum