theorem Th20: :: YELLOW10:20

for S, T being non empty reflexive antisymmetric up-complete RelStr
for x, y being Element of [:S,T:] st x << y holds
( x `1 << y `1 & x `2 << y `2 )