take union {{x1,x2},{x3}} ; :: thesis: for x being object holds
( x in union {{x1,x2},{x3}} iff ( x = x1 or x = x2 or x = x3 ) )
let x be object ; :: thesis: ( x in union {{x1,x2},{x3}} iff ( x = x1 or x = x2 or x = x3 ) )
( x in {x1,x2} iff ( x = x1 or x = x2 ) ) by TARSKI:def 2;
hence ( x in union {{x1,x2},{x3}} iff ( x = x1 or x = x2 or x = x3 ) ) by Lm1; :: thesis: verum