:: deftheorem Def1 defines [" YELLOW_3:def 1 :
for P, R, b₃ being Relation holds
( b₃ = ["P,R"] iff for x, y being object holds
( [x,y] in b₃ iff ex p, q, s, t being object st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) ) );