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

proof

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

end;

consider f being Function of [:(Pr D),(Pr D):],(Pr D) such that
A6: for x, y being object st x in Pr D & y in Pr D holds
S₁[x,y,f . (x,y)] from BINOP_1:sch 1(A5);
take f ; :: thesis: for p, q being PartialPredicate of D holds f . (p,q) = PP_or (p,q)
let p, q be PartialPredicate of D; :: thesis: f . (p,q) = PP_or (p,q)
( p in Pr D & q in Pr D ) by PARTFUN1:45;
hence f . (p,q) = PP_or (p,q) by A6; :: thesis: verum