let P, Q be PartialPredicate of D; :: thesis: ( P = (PPnegation D) . Q implies Q = (PPnegation D) . P )
assume A1: P = (PPnegation D) . Q ; :: thesis: Q = (PPnegation D) . P
set Z = (PPnegation D) . P;
A2: dom P = dom Q by A1, Def2;
hence dom Q = dom ((PPnegation D) . P) by Def2; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom Q or Q . b₁ = ((PPnegation D) . P) . b₁ )
let x be object ; :: thesis: ( not x in dom Q or Q . x = ((PPnegation D) . P) . x )
assume A3: x in dom Q ; :: thesis: Q . x = ((PPnegation D) . P) . x

per cases then ( P . x = FALSE or P . x = TRUE ) by A2, Th3;

suppose A4: P . x = FALSE ; :: thesis: Q . x = ((PPnegation D) . P) . x

Q . x = TRUE

proof

assume Q . x <> TRUE ; :: thesis: contradiction
then Q . x = FALSE by A3, Th3;
hence contradiction by A1, A3, A4, Def2; :: thesis: verum

end;

hence Q . x = ((PPnegation D) . P) . x by A2, A3, A4, Def2; :: thesis: verum

end;

suppose A5: P . x = TRUE ; :: thesis: Q . x = ((PPnegation D) . P) . x

Q . x = FALSE

proof

assume Q . x <> FALSE ; :: thesis: contradiction
then Q . x = TRUE by A3, Th3;
hence contradiction by A1, A3, A5, Def2; :: thesis: verum

end;

hence Q . x = ((PPnegation D) . P) . x by A2, A3, A5, Def2; :: thesis: verum

end;

end;