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 b1 being object holds
( not b1 in dom Q or Q . b1 = ((PPnegation D) . P) . b1 )
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;