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