:: deftheorem Def6 defines (#) RELAT_1:def 8 :
for P, R being set
for b₃ being Relation holds
( b₃ = P (#) R iff for x, y being object holds
( [x,y] in b₃ iff ex z being object st
( [x,z] in P & [z,y] in R ) ) );