let C be non empty set ; :: thesis: for f, g being Membership_Func of C holds 1_minus f c=
let f, g be Membership_Func of C; :: thesis: 1_minus f c=
max (f,g) c= by Th18;
hence 1_minus f c= by Th39; :: thesis: verum