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:21;
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 that
A2: x in field R and
A3: for y being set st y in field R & y <> x holds
[x,y] in R ; :: according to ORDERS_1:def 15 :: thesis: x is_superior_of R ~
thus x in field (R ~) by A2, RELAT_1:21; :: according to ORDERS_1:def 14 :: 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 that
A4: y in field (R ~) and
A5: y <> x ; :: thesis: [y,x] in R ~
[x,y] in R by A1, A3, A4, A5;
hence [y,x] in R ~ by RELAT_1:def 7; :: thesis: verum

end;

assume that
A6: x in field (R ~) and
A7: for y being set st y in field (R ~) & y <> x holds
[y,x] in R ~ ; :: according to ORDERS_1:def 14 :: thesis: x is_inferior_of R
thus x in field R by A6, RELAT_1:21; :: according to ORDERS_1:def 15 :: 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 that
A8: y in field R and
A9: y <> x ; :: thesis: [x,y] in R
[y,x] in R ~ by A1, A7, A8, A9;
hence [x,y] in R by RELAT_1:def 7; :: thesis: verum