take
union {{x1,x2,x3},{x4}}
; for x being object holds
( x in union {{x1,x2,x3},{x4}} iff ( x = x1 or x = x2 or x = x3 or x = x4 ) )
let x be object ; ( x in union {{x1,x2,x3},{x4}} iff ( x = x1 or x = x2 or x = x3 or x = x4 ) )
( x in {x1,x2,x3} iff ( x = x1 or x = x2 or x = x3 ) )
by Def1;
hence
( x in union {{x1,x2,x3},{x4}} iff ( x = x1 or x = x2 or x = x3 or x = x4 ) )
by Lm1; verum