not the carrier of R c= SQ R by defqc;
then consider a being Element of R such that
A: not a in SQ R ;
SQ R = { x where x is Element of R : x is square } by REALALG1:def 10;
then not a is square by A;
hence not for b₁ being Element of R holds b₁ is square ; :: thesis: verum