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