let F be preordered Field; :: thesis: for P being Preordering of F
for a, b being non zero Element of F st 0. F <= P,a & 0. F <= P,b 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 0. F <= P,a & 0. F <= P,b holds
( a <= P,b iff b " <= P,a " )
let a, b be non zero Element of F; :: thesis: ( 0. F <= P,a & 0. F <= P,b implies ( a <= P,b iff b " <= P,a " ) )
assume AS: ( 0. F <= P,a & 0. F <= P,b ) ; :: thesis: ( a <= P,b iff b " <= P,a " )
then X: ( 0. F <= P,a " & 0. F <= P,b " ) by REALALG1:27;
Y: ( a <> 0. F & b <> 0. F ) ;
hereby :: thesis: ( b " <= P,a " implies a <= P,b )
assume a <= P,b ; :: thesis: b " <= P,a "
then a * (a ") <= P,b * (a ") by X, c5;
then 1. F <= P,b * (a ") by Y, VECTSP_1:def 10;
then (1. F) * (b ") <= P,(b * (a ")) * (b ") by X, c5;
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 (b ") * b <= P,(a ") * b by AS, c5;
then 1. F <= P,(a ") * b by Y, VECTSP_1:def 10;
then (1. F) * a <= P,((a ") * b) * a by AS, c5;
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