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 )

proof

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;

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