let x, y, z be set ; :: thesis: ( [z,1] in x U+ y iff z in x )
x U+ y = [:x,{1}:] \/ [:y,{2}:] by Th74;
then ( [z,1] in x U+ y iff ( [z,1] in [:x,{1}:] or ( [z,1] in [:y,{2}:] & 1 <> 2 ) ) ) by XBOOLE_0:def 3;
hence ( [z,1] in x U+ y iff z in x ) by ZFMISC_1:129; :: thesis: verum