defpred S1[ 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 & S1[x,y,z] )
proof
let x,
y be
object ;
( x in Pr D & y in Pr D implies ex z being object st
( z in Pr D & S1[x,y,z] ) )
assume
x in Pr D
;
( not y in Pr D or ex z being object st
( z in Pr D & S1[x,y,z] ) )
then reconsider x =
x as
PartialPredicate of
D by PARTFUN1:46;
assume
y in Pr D
;
ex z being object st
( z in Pr D & S1[x,y,z] )
then reconsider y =
y as
PartialPredicate of
D by PARTFUN1:46;
take
PP_or (
x,
y)
;
( PP_or (x,y) in Pr D & S1[x,y, PP_or (x,y)] )
thus
(
PP_or (
x,
y)
in Pr D &
S1[
x,
y,
PP_or (
x,
y)] )
by PARTFUN1:45;
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
S1[x,y,f . (x,y)]
from BINOP_1:sch 1(A5);
take
f
; for p, q being PartialPredicate of D holds f . (p,q) = PP_or (p,q)
let p, q be PartialPredicate of D; 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; verum