let x be object ; :: thesis: ( x in {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} iff x in {x1,x2,x3,x4,x5,x6,x7,x8,x9} \/ {x10} )
A1: ( x in {x10} iff x = x10 ) by TARSKI:def 1;
( ( ( not x = x1 & not x = x2 & not x = x3 & not x = x4 & not x = x5 & not x = x6 & not x = x7 & not x = x8 & not x = x9 & not x = x10 ) or x in {x1,x2,x3,x4,x5,x6,x7,x8,x9} or x = x10 ) & ( ( not x in {x1,x2,x3,x4,x5,x6,x7,x8,x9} & not x = x10 ) or 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 Def7;
hence ( x in {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} iff x in {x1,x2,x3,x4,x5,x6,x7,x8,x9} \/ {x10} ) by A1, Def8, XBOOLE_0:def 3; :: thesis: verum