let R be preordered Ring; :: thesis: for P being Preordering of R
for a being Element of R st a in (- P) \ {(0. R)} holds
not a is square
let P be Preordering of R; :: thesis: for a being Element of R st a in (- P) \ {(0. R)} holds
not a is square
let a be Element of R; :: thesis: ( a in (- P) \ {(0. R)} implies not a is square )
assume a in (- P) \ {(0. R)} ; :: thesis: not a is square
then A: ( a in - P & not a in {(0. R)} ) by XBOOLE_0:def 5;
B: ( SQ R c= P & P /\ (- P) = {(0. R)} ) by REALALG1:def 14;
assume a is square ; :: thesis: contradiction
then a in SQ R ;
hence contradiction by A, B; :: thesis: verum