let h1, h2 be Membership_Func of C; :: thesis: ( ( for c being Element of C holds h1 . c = 1 - (h2 . c) ) implies for c being Element of C holds h2 . c = 1 - (h1 . c) )
assume A17: for c being Element of C holds h1 . c = 1 - (h2 . c) ; :: thesis: for c being Element of C holds h2 . c = 1 - (h1 . c)
let c be Element of C; :: thesis: h2 . c = 1 - (h1 . c)
thus h2 . c = 1 - (1 - (h2 . c))
.= 1 - (h1 . c) by A17 ; :: thesis: verum