set t = the Element of T;
per cases ( T = {} or T <> {} ) ;
suppose T = {} ; :: thesis: for b1 being set st b1 = x \+\ y holds
b1 is empty
then ( x = {} & y = {} ) by SUBSET_1:def 1;
hence for b1 being set st b1 = x \+\ y holds
b1 is empty ; :: thesis: verum
end;
suppose T <> {} ; :: thesis: for b1 being set st b1 = x \+\ y holds
b1 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 b1 being set st b1 = x \+\ y holds
b1 is empty ; :: thesis: verum
end;
end;