:: deftheorem Def1 defines Q. QUOFIELD:def 1 :
for I being non empty ZeroStr
for b₂ being Subset of [: the carrier of I, the carrier of I:] holds
( b₂ = Q. I iff for u being set holds
( u in b₂ iff ex a, b being Element of I st
( u = [a,b] & b <> 0. I ) ) );