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:38;
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 A2: ( x in field R & ( 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 12 :: thesis: x is_maximal_in R ~
hence x in field (R ~ ) by RELAT_1:38; :: according to ORDERS_1:def 11 :: 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 ( y in field (R ~ ) & y <> x ) ; :: thesis: not [x,y] in R ~
then not [y,x] in R by A1, A2;
hence not [x,y] in R ~ by RELAT_1:def 7; :: thesis: verum

end;

assume A3: ( x in field (R ~ ) & ( 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 11 :: thesis: x is_minimal_in R
hence x in field R by RELAT_1:38; :: according to ORDERS_1:def 12 :: 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 ( y in field R & y <> x ) ; :: thesis: not [y,x] in R
then not [x,y] in R ~ by A1, A3;
hence not [y,x] in R by RELAT_1:def 7; :: thesis: verum