let R be Relation; :: thesis: for x being set holds
( x is_minimal_in R ~ iff x is_maximal_in R )
let x be set ; :: thesis: ( x is_minimal_in R ~ iff x is_maximal_in R )
A1: field R = field (R ~) by RELAT_1:21;
thus ( x is_minimal_in R ~ implies x is_maximal_in R ) :: thesis: ( x is_maximal_in R implies x is_minimal_in R ~ )

proof

assume that
A2: x in field (R ~) and
A3: for y being set holds
( not y in field (R ~) or not y <> x or not [y,x] in R ~ ) ; :: according to ORDERS_1:def 13 :: thesis: x is_maximal_in R
thus x in field R by A2, RELAT_1:21; :: according to ORDERS_1:def 12 :: thesis: for y being set holds
( not y in field R or not y <> x or not [x,y] in R )
let y be set ; :: thesis: ( not y in field R or not y <> x or not [x,y] in R )
assume that
A4: y in field R and
A5: y <> x ; :: thesis: not [x,y] in R
not [y,x] in R ~ by A1, A3, A4, A5;
hence not [x,y] in R by RELAT_1:def 7; :: thesis: verum

end;

assume that
A6: x in field R and
A7: for y being set holds
( not y in field R or not y <> x or not [x,y] in R ) ; :: according to ORDERS_1:def 12 :: thesis: x is_minimal_in R ~
thus x in field (R ~) by A6, RELAT_1:21; :: according to ORDERS_1:def 13 :: thesis: for y being set holds
( not y in field (R ~) or not y <> x or not [y,x] in R ~ )
let y be set ; :: thesis: ( not y in field (R ~) or not y <> x or not [y,x] in R ~ )
assume that
A8: y in field (R ~) and
A9: y <> x ; :: thesis: not [y,x] in R ~
not [x,y] in R by A1, A7, A8, A9;
hence not [y,x] in R ~ by RELAT_1:def 7; :: thesis: verum