let C be non empty set ; :: thesis: for f, g being Membership_Func of C holds 1_minus (f \ g) = max ((1_minus f),g)
let f, g be Membership_Func of C; :: thesis: 1_minus (f \ g) = max ((1_minus f),g)
thus 1_minus (f \ g) = max ((1_minus f),(1_minus (1_minus g))) by FUZZY_1:11
.= max ((1_minus f),g) ; :: thesis: verum