for L being RelStr
for X being Subset of L
for Y being Subset of (L opp) st X = Y holds
( downarrow X = uparrow Y & uparrow X = downarrow Y )