take union {{x1,x2,x3,x4,x5,x6,x7,x8,x9},{x10}} ; :: thesis: for x being object holds
( x in union {{x1,x2,x3,x4,x5,x6,x7,x8,x9},{x10}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 or x = x10 ) )
let x be object ; :: thesis: ( x in union {{x1,x2,x3,x4,x5,x6,x7,x8,x9},{x10}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 or x = x10 ) )
( x in {x1,x2,x3,x4,x5,x6,x7,x8,x9} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 ) ) by Def7;
hence ( x in union {{x1,x2,x3,x4,x5,x6,x7,x8,x9},{x10}} iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 or x = x9 or x = x10 ) ) by Lm1; :: thesis: verum