for S1, S2 being non empty RelStr
for a, c being Element of S1
for b, d being Element of S2 holds
( ( a <= c & b <= d ) iff [a,b] <= [c,d] )