let F be preordered Field; :: thesis: for P being Preordering of F
for a being non zero Element of F st a in P holds
a " in P
let P be Preordering of F; :: thesis: for a being non zero Element of F st a in P holds
a " in P
let a be non zero Element of F; :: thesis: ( a in P implies a " in P )
assume A: a in P ; :: thesis: a " in P
E: a <> 0. F ;
set b = a " ;
C: P * P c= P by defppc;
(a ") * (a ") = (a ") ^2 ;
then (a ") * (a ") in P by ord1;
then B: a * ((a ") * (a ")) in { (x * y) where x, y is Element of F : ( x in P & y in P ) } by A;
a * ((a ") * (a ")) = (a * (a ")) * (a ") by GROUP_1:def 3
.= (1. F) * (a ") by E, VECTSP_1:def 10
.= a " ;
hence a " in P by B, C; :: thesis: verum