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 " = b " implies a = b )

proof

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

end;

hence ( a < P,b iff b " < P,a " ) by AS, fi2; :: thesis: verum