let R be preordered Ring; :: thesis: for P being Preordering of R
for a being Element of R holds
( a is P -positive iff 0. R < P,a )
let P be Preordering of R; :: thesis: for a being Element of R holds
( a is P -positive iff 0. R < P,a )
let a be Element of R; :: thesis: ( a is P -positive iff 0. R < P,a )

hereby :: thesis: ( 0. R < P,a implies a is P -positive )

assume a is P -positive ; :: thesis: 0. R < P,a
then ( a in P & not a in {(0. R)} ) by XBOOLE_0:def 5;
then ( 0. R <= P,a & a <> 0. R ) by TARSKI:def 1;
hence 0. R < P,a ; :: thesis: verum

end;

assume 0. R < P,a ; :: thesis: a is P -positive
then ( 0. R <= P,a & a <> 0. R ) ;
then ( a in P & not a in {(0. R)} ) by TARSKI:def 1;
hence a is P -positive by XBOOLE_0:def 5; :: thesis: verum