:: deftheorem Def5 defines -^ ORDINAL3:def 5 :
for A, B, b₃ being Ordinal holds
( ( B c= A implies ( b₃ = A -^ B iff A = B +^ b₃ ) ) & ( not B c= A implies ( b₃ = A -^ B iff b₃ = {} ) ) );