for a, b being set holds
( not MODADD2 (a,b) is empty iff ( ( not a is empty or not b is empty ) & ( a is empty or b is empty ) ) ) by Def34;