:: deftheorem Def9 defines Connection WAYBEL_1:def 9 :
for S, T being RelStr
for b₃ being set holds
( b₃ is Connection of S,T iff ex g being Function of S,T ex d being Function of T,S st b₃ = [g,d] );