let F be preordered Field; 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; 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; ( 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 )
; ( 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 ( b " <= P,a " implies a <= P,b )
assume
a <= P,
b
;
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 "
;
verum
end;
assume
b " <= P,a "
; 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
; verum