theorem :: ORDERS_1:62

for R being Relation
for x being set holds
( x is_inferior_of R ~ iff x is_superior_of R )