defpred S₁[ object , object ] means for p being PartialPredicate of D st p = $1 holds
$2 = PP_not p;
A9: for x being object st x in Pr D holds
ex z being object st
( z in Pr D & S₁[x,z] )

proof

let x be object ; :: thesis: ( x in Pr D implies ex z being object st
( z in Pr D & S₁[x,z] ) )
assume x in Pr D ; :: thesis: ex z being object st
( z in Pr D & S₁[x,z] )
then reconsider x = x as PartialPredicate of D by PARTFUN1:46;
take PP_not x ; :: thesis: ( PP_not x in Pr D & S₁[x, PP_not x] )
thus ( PP_not x in Pr D & S₁[x, PP_not x] ) by PARTFUN1:45; :: thesis: verum

end;

consider f being Function of (Pr D),(Pr D) such that
A10: for x being object st x in Pr D holds
S₁[x,f . x] from FUNCT_2:sch 1(A9);
take f ; :: thesis: for p being PartialPredicate of D holds f . p = PP_not p
thus for p being PartialPredicate of D holds f . p = PP_not p by A10, PARTFUN1:45; :: thesis: verum