let x1, x2, x3, x4, x5, x6, x7, x8, x9, x10 be object ; :: thesis: {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} = {x2,x3,x4,x5,x6,x7,x8,x9,x10} \/ {x1}

now :: thesis: for x being object holds
( x in {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} iff x in {x2,x3,x4,x5,x6,x7,x8,x9,x10} \/ {x1} )

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

end;

hence {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} = {x2,x3,x4,x5,x6,x7,x8,x9,x10} \/ {x1} by TARSKI:2; :: thesis: verum