for S, T being non empty reflexive antisymmetric up-complete RelStr
for a, c being Element of S
for b, d being Element of T st [a,b] << [c,d] holds
( a << c & b << d )