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