theorem :: ORDERS_1:61

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