let R be Ring; :: thesis: for S being Subring of R holds SQ S c= SQ R
let S be Subring of R; :: thesis: SQ S c= SQ R
AS4: the carrier of S c= the carrier of R by C0SP1:def 3;
let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in SQ S or o in SQ R )
assume o in SQ S ; :: thesis: o in SQ R
then consider a being Element of S such that
A: ( o = a & a is square ) ;
consider b being Element of S such that
B: a = b ^2 by A;
reconsider a1 = a, b1 = b as Element of R by AS4;
dom the multF of S = [: the carrier of S, the carrier of S:] by FUNCT_2:def 1;
then B6: [b,b] in dom the multF of S ;
a1 = ( the multF of R || the carrier of S) . (b,b) by C0SP1:def 3, B
.= b1 ^2 by B6, FUNCT_1:49 ;
then a1 is square ;
hence o in SQ R by A; :: thesis: verum