let R be Relation; :: thesis: for x being set holds
( x is_inferior_of R iff x is_superior_of R ~ )
let x be set ; :: thesis: ( x is_inferior_of R iff x is_superior_of R ~ )
A1: field R = field (R ~ ) by RELAT_1:38;
thus ( x is_inferior_of R implies x is_superior_of R ~ ) :: thesis: ( x is_superior_of R ~ implies x is_inferior_of R )

proof

assume A2: ( x in field R & ( for y being set st y in field R & y <> x holds
[x,y] in R ) ) ; :: according to ORDERS_1:def 14 :: thesis: x is_superior_of R ~
hence x in field (R ~ ) by RELAT_1:38; :: according to ORDERS_1:def 13 :: thesis: for y being set st y in field (R ~ ) & y <> x holds
[y,x] in R ~
let y be set ; :: thesis: ( y in field (R ~ ) & y <> x implies [y,x] in R ~ )
assume ( y in field (R ~ ) & y <> x ) ; :: thesis: [y,x] in R ~
then [x,y] in R by A1, A2;
hence [y,x] in R ~ by RELAT_1:def 7; :: thesis: verum

end;

assume A3: ( x in field (R ~ ) & ( for y being set st y in field (R ~ ) & y <> x holds
[y,x] in R ~ ) ) ; :: according to ORDERS_1:def 13 :: thesis: x is_inferior_of R
hence x in field R by RELAT_1:38; :: according to ORDERS_1:def 14 :: thesis: for y being set st y in field R & y <> x holds
[x,y] in R
let y be set ; :: thesis: ( y in field R & y <> x implies [x,y] in R )
assume ( y in field R & y <> x ) ; :: thesis: [x,y] in R
then [y,x] in R ~ by A1, A3;
hence [x,y] in R by RELAT_1:def 7; :: thesis: verum