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:12
.= max (1_minus f),g ; :: thesis: verum