:: deftheorem Def8 defines q0. QUOFIELD:def 8 :
for I being non degenerated commutative domRing-like Ring
for b₂ being Element of Quot. I holds
( b₂ = q0. I iff for z being Element of Q. I holds
( z in b₂ iff z `1 = 0. I ) );