theorem :: YELLOW_7:20

for L being non empty RelStr
for x being Element of L
for y being Element of (L opp) st x = y holds
( downarrow x = uparrow y & uparrow x = downarrow y ) by Th19;