let R be preordered Ring; :: thesis: for P being Preordering of R
for a being Element of R holds
( a is P -negative iff a < P, 0. R )
let P be Preordering of R; :: thesis: for a being Element of R holds
( a is P -negative iff a < P, 0. R )
let a be Element of R; :: thesis: ( a is P -negative iff a < P, 0. R )
hereby :: thesis: ( a < P, 0. R implies a is P -negative )
assume a is P -negative ; :: thesis: a < P, 0. R
then ( a in - P & not a in {(0. R)} ) by XBOOLE_0:def 5;
then ( - a in - (- P) & not a in {(0. R)} ) ;
then ( a <= P, 0. R & a <> 0. R ) by TARSKI:def 1;
hence a < P, 0. R ; :: thesis: verum
end;
assume a < P, 0. R ; :: thesis: a is P -negative
then ( a <= P, 0. R & a <> 0. R ) ;
then ( - (- a) in - P & not a in {(0. R)} ) by TARSKI:def 1;
hence a is P -negative by XBOOLE_0:def 5; :: thesis: verum