:: deftheorem Def1 defines Element SUBSET_1:def 1 :
for X, b₂ being set holds
( ( not X is empty implies ( b₂ is Element of X iff b₂ in X ) ) & ( X is empty implies ( b₂ is Element of X iff b₂ is empty ) ) );