set t = the Element of T;

per cases ( T = {} or T <> {} ) ;

suppose T = {} ; :: thesis: for b₁ being set st b₁ = x \+\ y holds
b₁ is empty

then ( x = {} & y = {} ) by SUBSET_1:def 1;
hence for b₁ being set st b₁ = x \+\ y holds
b₁ is empty ; :: thesis: verum

end;

suppose T <> {} ; :: thesis: for b₁ being set st b₁ = x \+\ y holds
b₁ is empty

then consider t being object such that
A1: T = {t} by ZFMISC_1:131;
x = t by A1, TARSKI:def 1
.= y by A1, TARSKI:def 1 ;
hence for b₁ being set st b₁ = x \+\ y holds
b₁ is empty ; :: thesis: verum

end;

end;