let C be non empty set ; :: thesis: for f, g being Membership_Func of C st min (f,g) = EMF C holds
f \ g = f

let f, g be Membership_Func of C; :: thesis: ( min (f,g) = EMF C implies f \ g = f )
A1: C = dom f by FUNCT_2:def 1;
assume A2: min (f,g) = EMF C ; :: thesis: f \ g = f
A3: for x being Element of C st x in C holds
(min (f,())) . x = f . x
proof
let x be Element of C; :: thesis: ( x in C implies (min (f,())) . x = f . x )
A4: (EMF C) . x = min ((f . x),(g . x)) by ;
per cases ( f . x = (EMF C) . x or g . x = (EMF C) . x ) by ;
suppose A5: f . x = (EMF C) . x ; :: thesis: ( x in C implies (min (f,())) . x = f . x )
(min (f,())) . x = min ((f . x),(() . x)) by FUZZY_1:5
.= (min ((),(EMF C))) . x by
.= (EMF C) . x by FUZZY_1:18 ;
hence ( x in C implies (min (f,())) . x = f . x ) by A5; :: thesis: verum
end;
suppose A6: g . x = (EMF C) . x ; :: thesis: ( x in C implies (min (f,())) . x = f . x )
(min (f,())) . x = min ((f . x),(() . x)) by FUZZY_1:5
.= min ((f . x),(1 - ((EMF C) . x))) by
.= min ((f . x),((1_minus (EMF C)) . x)) by FUZZY_1:def 5
.= min ((f . x),((UMF C) . x)) by FUZZY_1:40
.= (min (f,(UMF C))) . x by FUZZY_1:5 ;
hence ( x in C implies (min (f,())) . x = f . x ) by FUZZY_1:18; :: thesis: verum
end;
end;
end;
C = dom (min (f,())) by FUNCT_2:def 1;
hence f \ g = f by ; :: thesis: verum