let R be non degenerated preordered Ring; :: thesis: for P being Preordering of R holds
( 0. R < P, 1. R & - (1. R) < P, 0. R )
let P be Preordering of R; :: thesis: ( 0. R < P, 1. R & - (1. R) < P, 0. R )
0. R <= P, 1. R by REALALG1:25;
hence 0. R < P, 1. R ; :: thesis: - (1. R) < P, 0. R
- (1. R) <= P, 0. R by REALALG1:25;
hence - (1. R) < P, 0. R ; :: thesis: verum