let R be preordered Ring; :: thesis: for P being Preordering of R holds (- P) /\ (SQ R) = {(0. R)}
let P be Preordering of R; :: thesis: (- P) /\ (SQ R) = {(0. R)}
0. R in P by REALALG1:25;
then C: - (0. R) in - P ;
A: now :: thesis: for o being object st o in {(0. R)} holds
o in (- P) /\ (SQ R)
let o be object ; :: thesis: ( o in {(0. R)} implies o in (- P) /\ (SQ R) )
assume o in {(0. R)} ; :: thesis: o in (- P) /\ (SQ R)
then o = 0. R by TARSKI:def 1;
then ( o in - P & o in SQ R ) by C;
hence o in (- P) /\ (SQ R) ; :: thesis: verum
end;
now :: thesis: for o being object st o in (- P) /\ (SQ R) holds
o in {(0. R)}
let o be object ; :: thesis: ( o in (- P) /\ (SQ R) implies o in {(0. R)} )
assume o in (- P) /\ (SQ R) ; :: thesis: o in {(0. R)}
then H0: ( o in - P & o in SQ R ) by XBOOLE_0:def 4;
then consider a being Element of R such that
H1: ( o = a & a is square ) ;
not a in (- P) \ {(0. R)} by H1, sq5;
hence o in {(0. R)} by H0, H1, XBOOLE_0:def 5; :: thesis: verum
end;
hence (- P) /\ (SQ R) = {(0. R)} by A, TARSKI:2; :: thesis: verum