let a be Element of R; :: thesis: ( not a is P -positive & a is square implies a is zero )
assume AS: ( not a is P -positive & a is square ) ; :: thesis: a is zero
then ( not a in P or a in {(0. R)} ) by XBOOLE_0:def 5;

per cases then ( not a in P or a = 0. R ) by TARSKI:def 1;

suppose B: not a in P ; :: thesis: a is zero

C: a in SQ R by AS;
D: SQ R c= QS R by REALALG1:18;
QS R c= P by REALALG1:24;
hence a is zero by B, C, D; :: thesis: verum

end;

suppose a = 0. R ; :: thesis: a is zero

hence a is zero ; :: thesis: verum

end;

end;