let R be Ring; :: thesis: SQ R c= QS R
let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in SQ R or o in QS R )
assume o in SQ R ; :: thesis: o in QS R
then consider a being Element of R such that
A: ( o = a & a is square ) ;
thus o in QS R by A; :: thesis: verum