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 Th39

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

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

.= 1_minus f by Th17 ; :: thesis: verum

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 Th39

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

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

.= 1_minus f by Th17 ; :: thesis: verum