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