let F be preordered Field; :: thesis: for P being Preordering of F
for a, b being non zero Element of F st a <= P, 0. F & b <= P, 0. F holds
( a <= P,b iff b " <= P,a " )
let P be Preordering of F; :: thesis: for a, b being non zero Element of F st a <= P, 0. F & b <= P, 0. F holds
( a <= P,b iff b " <= P,a " )
let a, b be non zero Element of F; :: thesis: ( a <= P, 0. F & b <= P, 0. F implies ( a <= P,b iff b " <= P,a " ) )
assume AS: ( a <= P, 0. F & b <= P, 0. F ) ; :: thesis: ( a <= P,b iff b " <= P,a " )
Y: ( a <> 0. F & b <> 0. F ) ;
( - a <> - (0. F) & - b <> - (0. F) ) ;
then ( not - a is zero & not - b is zero ) ;
then ( - ((- a) ") <= P, - (0. F) & - ((- b) ") <= P, - (0. F) ) by AS, REALALG1:27;
then X: ( a " <= P, - (0. F) & b " <= P, - (0. F) ) by YZ;

hereby :: thesis: ( b " <= P,a " implies a <= P,b )

assume a <= P,b ; :: thesis: b " <= P,a "
then b * (a ") <= P,a * (a ") by X, c55;
then b * (a ") <= P, 1. F by Y, VECTSP_1:def 10;
then (1. F) * (b ") <= P,(b * (a ")) * (b ") by X, c55;
then b " <= P,((b ") * b) * (a ") by GROUP_1:def 3;
then b " <= P,(1. F) * (a ") by Y, VECTSP_1:def 10;
hence b " <= P,a " ; :: thesis: verum

end;

assume b " <= P,a " ; :: thesis: a <= P,b
then (a ") * b <= P,(b ") * b by AS, c55;
then (a ") * b <= P, 1. F by Y, VECTSP_1:def 10;
then (1. F) * a <= P,((a ") * b) * a by AS, c55;
then a <= P,((a ") * a) * b by GROUP_1:def 3;
then a <= P,(1. F) * b by Y, VECTSP_1:def 10;
hence a <= P,b ; :: thesis: verum