theorem :: YELLOW10:38

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