let x1, x2, x3, x4, x5 be object ; {x1,x2,x3,x4,x5} = {x1,x2,x3} \/ {x4,x5}
now for x being object holds
( x in {x1,x2,x3,x4,x5} iff x in {x1,x2,x3} \/ {x4,x5} )let x be
object ;
( x in {x1,x2,x3,x4,x5} iff x in {x1,x2,x3} \/ {x4,x5} )
(
x in {x1,x2,x3,x4,x5} iff (
x = x1 or
x = x2 or
x = x3 or
x = x4 or
x = x5 ) )
by Def3;
then
(
x in {x1,x2,x3,x4,x5} iff (
x in {x1,x2,x3} or
x in {x4,x5} ) )
by Def1, TARSKI:def 2;
hence
(
x in {x1,x2,x3,x4,x5} iff
x in {x1,x2,x3} \/ {x4,x5} )
by XBOOLE_0:def 3;
verum end;
hence
{x1,x2,x3,x4,x5} = {x1,x2,x3} \/ {x4,x5}
by TARSKI:2; verum