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

let f be Membership_Func of C; :: thesis: f \+\ (EMF C) = f

thus f \+\ (EMF C) = max ((min (f,(UMF C))),(min ((1_minus f),(EMF C)))) by Th39

.= max (f,(min ((1_minus f),(EMF C)))) by Th17

.= max (f,(EMF C)) by Th17

.= f by Th17 ; :: thesis: verum

let f be Membership_Func of C; :: thesis: f \+\ (EMF C) = f

thus f \+\ (EMF C) = max ((min (f,(UMF C))),(min ((1_minus f),(EMF C)))) by Th39

.= max (f,(min ((1_minus f),(EMF C)))) by Th17

.= max (f,(EMF C)) by Th17

.= f by Th17 ; :: thesis: verum