for S, T being non empty up-complete Poset
for a, c being Element of S
for b, d being Element of T holds
( [a,b] << [c,d] iff ( a << c & b << d ) )