:: deftheorem Def6 defines div^ ORDINAL3:def 6 :
for A, B, b₃ being Ordinal holds
( ( B <> {} implies ( b₃ = A div^ B iff ex C being Ordinal st
( A = (b₃ *^ B) +^ C & C in B ) ) ) & ( not B <> {} implies ( b₃ = A div^ B iff b₃ = {} ) ) );