let D be non empty set ; :: thesis: for p being PartialPredicate of D

for d being Element of D holds

( d in dom p iff not d in dom (PP_inversion p) )

let p be PartialPredicate of D; :: thesis: for d being Element of D holds

( d in dom p iff not d in dom (PP_inversion p) )

let d be Element of D; :: thesis: ( d in dom p iff not d in dom (PP_inversion p) )

A1: dom (PP_inversion p) = { d where d is Element of D : not d in dom p } by Def19;

thus ( d in dom p implies not d in dom (PP_inversion p) ) :: thesis: ( not d in dom (PP_inversion p) implies d in dom p )

for d being Element of D holds

( d in dom p iff not d in dom (PP_inversion p) )

let p be PartialPredicate of D; :: thesis: for d being Element of D holds

( d in dom p iff not d in dom (PP_inversion p) )

let d be Element of D; :: thesis: ( d in dom p iff not d in dom (PP_inversion p) )

A1: dom (PP_inversion p) = { d where d is Element of D : not d in dom p } by Def19;

thus ( d in dom p implies not d in dom (PP_inversion p) ) :: thesis: ( not d in dom (PP_inversion p) implies d in dom p )

proof

thus
( not d in dom (PP_inversion p) implies d in dom p )
by A1; :: thesis: verum
assume A2:
d in dom p
; :: thesis: not d in dom (PP_inversion p)

assume d in dom (PP_inversion p) ; :: thesis: contradiction

then ex d1 being Element of D st

( d = d1 & not d1 in dom p ) by A1;

hence contradiction by A2; :: thesis: verum

end;assume d in dom (PP_inversion p) ; :: thesis: contradiction

then ex d1 being Element of D st

( d = d1 & not d1 in dom p ) by A1;

hence contradiction by A2; :: thesis: verum