let p be boolean-valued Function; :: thesis: for x being set st x in dom p holds
( ('not' p) . x = TRUE iff p . x = FALSE )
let x be set ; :: thesis: ( x in dom p implies ( ('not' p) . x = TRUE iff p . x = FALSE ) )
assume x in dom p ; :: thesis: ( ('not' p) . x = TRUE iff p . x = FALSE )
then ('not' p) . x = 'not' (p . x) by MARGREL1:def 17;
hence ( ('not' p) . x = TRUE iff p . x = FALSE ) ; :: thesis: verum