let x, y be set ; :: thesis: for z being object holds
( [z,1] in x U+ y iff z in x )
let z be object ; :: thesis: ( [z,1] in x U+ y iff z in x )
x U+ y = [:x,{1}:] \/ [:y,{2}:] by Th73;
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:106; :: thesis: verum