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 " = b " implies a = b )
hence
( a < P,b iff b " < P,a " )
by AS, fi2; verum