for S being non empty reflexive RelStr
for T being non empty RelStr
for x being Element of [:S,T:] holds proj2 (downarrow x) = downarrow (x `2)