theorem :: YELLOW11:13

for L being non empty reflexive transitive RelStr
for a, b being Element of L holds [#a,b#] = (uparrow a) /\ (downarrow b)