theorem lemquadr: :: FIELD_9:8

for R being domRing
for S being domRingExtension of R
for a being Element of R
for b being Element of S holds
( not b ^2 = a ^2 or b = a or b = - a )