theorem :: REALALG1:17

for R being Ring holds
( 0. R in SQ R & 1. R in SQ R ) ;