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

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