let C be non empty set ; :: thesis: for f being Membership_Func of C holds f \+\ (UMF C) = 1_minus f
let f be Membership_Func of C; :: thesis: f \+\ (UMF C) = 1_minus f
thus f \+\ (UMF C) = max (min f,(EMF C)),(min (1_minus f),(UMF C)) by Th44
.= max (EMF C),(min (1_minus f),(UMF C)) by Th19
.= min (1_minus f),(UMF C) by Th19
.= 1_minus f by Th19 ; :: thesis: verum