begin
Lm1:
for x, X, y being set holds
( x in union {X,{y}} iff ( x in X or x = y ) )
definition
let x1,
x2,
x3 be
set ;
func {x1,x2,x3} -> set means :
Def1:
for
x being
set holds
(
x in it iff (
x = x1 or
x = x2 or
x = x3 ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 ) )
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 ) ) ) & ( for x being set holds
( x in b2 iff ( x = x1 or x = x2 or x = x3 ) ) ) holds
b1 = b2
end;
::
deftheorem Def1 defines
{ ENUMSET1:def 1 :
for x1, x2, x3, b4 being set holds
( b4 = {x1,x2,x3} iff for x being set holds
( x in b4 iff ( x = x1 or x = x2 or x = x3 ) ) );
definition
let x1,
x2,
x3,
x4 be
set ;
func {x1,x2,x3,x4} -> set means :
Def2:
for
x being
set holds
(
x in it iff (
x = x1 or
x = x2 or
x = x3 or
x = x4 ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 ) )
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) ) & ( for x being set holds
( x in b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) ) holds
b1 = b2
end;
::
deftheorem Def2 defines
{ ENUMSET1:def 2 :
for x1, x2, x3, x4, b5 being set holds
( b5 = {x1,x2,x3,x4} iff for x being set holds
( x in b5 iff ( x = x1 or x = x2 or x = x3 or x = x4 ) ) );
definition
let x1,
x2,
x3,
x4,
x5 be
set ;
func {x1,x2,x3,x4,x5} -> set means :
Def3:
for
x being
set holds
(
x in it iff (
x = x1 or
x = x2 or
x = x3 or
x = x4 or
x = x5 ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) )
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) ) ) & ( for x being set holds
( x in b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) ) ) holds
b1 = b2
end;
::
deftheorem Def3 defines
{ ENUMSET1:def 3 :
for x1, x2, x3, x4, x5, b6 being set holds
( b6 = {x1,x2,x3,x4,x5} iff for x being set holds
( x in b6 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 ) ) );
definition
let x1,
x2,
x3,
x4,
x5,
x6 be
set ;
func {x1,x2,x3,x4,x5,x6} -> set means :
Def4:
for
x being
set holds
(
x in it iff (
x = x1 or
x = x2 or
x = x3 or
x = x4 or
x = x5 or
x = x6 ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) )
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) ) ) & ( for x being set holds
( x in b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) ) ) holds
b1 = b2
end;
::
deftheorem Def4 defines
{ ENUMSET1:def 4 :
for x1, x2, x3, x4, x5, x6, b7 being set holds
( b7 = {x1,x2,x3,x4,x5,x6} iff for x being set holds
( x in b7 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 ) ) );
definition
let x1,
x2,
x3,
x4,
x5,
x6,
x7 be
set ;
func {x1,x2,x3,x4,x5,x6,x7} -> set means :
Def5:
for
x being
set holds
(
x in it iff (
x = x1 or
x = x2 or
x = x3 or
x = x4 or
x = x5 or
x = x6 or
x = x7 ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) )
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) ) ) & ( for x being set holds
( x in b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) ) ) holds
b1 = b2
end;
::
deftheorem Def5 defines
{ ENUMSET1:def 5 :
for x1, x2, x3, x4, x5, x6, x7, b8 being set holds
( b8 = {x1,x2,x3,x4,x5,x6,x7} iff for x being set holds
( x in b8 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 ) ) );
definition
let x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 be
set ;
func {x1,x2,x3,x4,x5,x6,x7,x8} -> set means :
Def6:
for
x being
set holds
(
x in it iff (
x = x1 or
x = x2 or
x = x3 or
x = x4 or
x = x5 or
x = x6 or
x = x7 or
x = x8 ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 ) )
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 ) ) ) & ( for x being set holds
( x in b2 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 ) ) ) holds
b1 = b2
end;
::
deftheorem Def6 defines
{ ENUMSET1:def 6 :
for x1, x2, x3, x4, x5, x6, x7, x8, b9 being set holds
( b9 = {x1,x2,x3,x4,x5,x6,x7,x8} iff for x being set holds
( x in b9 iff ( x = x1 or x = x2 or x = x3 or x = x4 or x = x5 or x = x6 or x = x7 or x = x8 ) ) );
definition
let x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 be
set ;
func {x1,x2,x3,x4,x5,x6,x7,x8,x9} -> set means :
Def7:
for
x being
set holds
(
x in it 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 ) );
existence
ex b1 being set st
for x being set holds
( x in b1 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 ) )
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 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 ) ) ) & ( for x being set holds
( x in b2 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 ) ) ) holds
b1 = b2
end;
::
deftheorem Def7 defines
{ ENUMSET1:def 7 :
for x1, x2, x3, x4, x5, x6, x7, x8, x9, b10 being set holds
( b10 = {x1,x2,x3,x4,x5,x6,x7,x8,x9} iff for x being set holds
( x in b10 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 ) ) );
definition
let x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9,
x10 be
set ;
func {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} -> set means :
Def8:
for
x being
set holds
(
x in it 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 ) );
existence
ex b1 being set st
for x being set holds
( x in b1 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 ) )
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 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 ) ) ) & ( for x being set holds
( x in b2 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 ) ) ) holds
b1 = b2
end;
::
deftheorem Def8 defines
{ ENUMSET1:def 8 :
for x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, b11 being set holds
( b11 = {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} iff for x being set holds
( x in b11 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 ) ) );
Lm2:
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x1,x2} \/ {x3,x4}
theorem Th4:
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x1} \/ {x2,x3,x4}
theorem
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x1,x2} \/ {x3,x4} by Lm2;
theorem Th6:
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x1,x2,x3} \/ {x4}
Lm3:
for x1, x2, x3, x4, x5 being set holds {x1,x2,x3,x4,x5} = {x1,x2,x3} \/ {x4,x5}
theorem Th7:
for
x1,
x2,
x3,
x4,
x5 being
set holds
{x1,x2,x3,x4,x5} = {x1} \/ {x2,x3,x4,x5}
theorem Th8:
for
x1,
x2,
x3,
x4,
x5 being
set holds
{x1,x2,x3,x4,x5} = {x1,x2} \/ {x3,x4,x5}
theorem
for
x1,
x2,
x3,
x4,
x5 being
set holds
{x1,x2,x3,x4,x5} = {x1,x2,x3} \/ {x4,x5} by Lm3;
theorem Th10:
for
x1,
x2,
x3,
x4,
x5 being
set holds
{x1,x2,x3,x4,x5} = {x1,x2,x3,x4} \/ {x5}
Lm4:
for x1, x2, x3, x4, x5, x6 being set holds {x1,x2,x3,x4,x5,x6} = {x1,x2,x3} \/ {x4,x5,x6}
theorem Th11:
for
x1,
x2,
x3,
x4,
x5,
x6 being
set holds
{x1,x2,x3,x4,x5,x6} = {x1} \/ {x2,x3,x4,x5,x6}
theorem Th12:
for
x1,
x2,
x3,
x4,
x5,
x6 being
set holds
{x1,x2,x3,x4,x5,x6} = {x1,x2} \/ {x3,x4,x5,x6}
theorem
for
x1,
x2,
x3,
x4,
x5,
x6 being
set holds
{x1,x2,x3,x4,x5,x6} = {x1,x2,x3} \/ {x4,x5,x6} by Lm4;
theorem Th14:
for
x1,
x2,
x3,
x4,
x5,
x6 being
set holds
{x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4} \/ {x5,x6}
theorem
for
x1,
x2,
x3,
x4,
x5,
x6 being
set holds
{x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4,x5} \/ {x6}
Lm5:
for x1, x2, x3, x4, x5, x6, x7 being set holds {x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4} \/ {x5,x6,x7}
theorem Th16:
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set holds
{x1,x2,x3,x4,x5,x6,x7} = {x1} \/ {x2,x3,x4,x5,x6,x7}
theorem Th17:
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set holds
{x1,x2,x3,x4,x5,x6,x7} = {x1,x2} \/ {x3,x4,x5,x6,x7}
theorem Th18:
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set holds
{x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3} \/ {x4,x5,x6,x7}
theorem
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set holds
{x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4} \/ {x5,x6,x7} by Lm5;
theorem
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set holds
{x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4,x5} \/ {x6,x7}
theorem
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set holds
{x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4,x5,x6} \/ {x7}
Lm6:
for x1, x2, x3, x4, x5, x6, x7, x8 being set holds {x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8}
theorem
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set holds
{x1,x2,x3,x4,x5,x6,x7,x8} = {x1} \/ {x2,x3,x4,x5,x6,x7,x8}
theorem Th23:
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set holds
{x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2} \/ {x3,x4,x5,x6,x7,x8}
theorem Th24:
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set holds
{x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3} \/ {x4,x5,x6,x7,x8}
theorem
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set holds
{x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8} by Lm6;
theorem
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set holds
{x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4,x5} \/ {x6,x7,x8}
theorem
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set holds
{x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4,x5,x6} \/ {x7,x8}
theorem
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8 being
set holds
{x1,x2,x3,x4,x5,x6,x7,x8} = {x1,x2,x3,x4,x5,x6,x7} \/ {x8}
theorem Th30:
for
x1,
x2 being
set holds
{x1,x1,x2} = {x1,x2}
theorem Th31:
for
x1,
x2,
x3 being
set holds
{x1,x1,x2,x3} = {x1,x2,x3}
theorem Th32:
for
x1,
x2,
x3,
x4 being
set holds
{x1,x1,x2,x3,x4} = {x1,x2,x3,x4}
theorem Th33:
for
x1,
x2,
x3,
x4,
x5 being
set holds
{x1,x1,x2,x3,x4,x5} = {x1,x2,x3,x4,x5}
theorem Th34:
for
x1,
x2,
x3,
x4,
x5,
x6 being
set holds
{x1,x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4,x5,x6}
theorem Th35:
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set holds
{x1,x1,x2,x3,x4,x5,x6,x7} = {x1,x2,x3,x4,x5,x6,x7}
theorem
for
x1 being
set holds
{x1,x1,x1} = {x1}
theorem Th37:
for
x1,
x2 being
set holds
{x1,x1,x1,x2} = {x1,x2}
theorem Th38:
for
x1,
x2,
x3 being
set holds
{x1,x1,x1,x2,x3} = {x1,x2,x3}
theorem Th39:
for
x1,
x2,
x3,
x4 being
set holds
{x1,x1,x1,x2,x3,x4} = {x1,x2,x3,x4}
theorem Th40:
for
x1,
x2,
x3,
x4,
x5 being
set holds
{x1,x1,x1,x2,x3,x4,x5} = {x1,x2,x3,x4,x5}
theorem Th41:
for
x1,
x2,
x3,
x4,
x5,
x6 being
set holds
{x1,x1,x1,x2,x3,x4,x5,x6} = {x1,x2,x3,x4,x5,x6}
theorem
for
x1 being
set holds
{x1,x1,x1,x1} = {x1}
theorem Th43:
for
x1,
x2 being
set holds
{x1,x1,x1,x1,x2} = {x1,x2}
theorem Th44:
for
x1,
x2,
x3 being
set holds
{x1,x1,x1,x1,x2,x3} = {x1,x2,x3}
theorem Th45:
for
x1,
x2,
x3,
x4 being
set holds
{x1,x1,x1,x1,x2,x3,x4} = {x1,x2,x3,x4}
theorem Th46:
for
x1,
x2,
x3,
x4,
x5 being
set holds
{x1,x1,x1,x1,x2,x3,x4,x5} = {x1,x2,x3,x4,x5}
theorem
for
x1 being
set holds
{x1,x1,x1,x1,x1} = {x1}
theorem Th48:
for
x1,
x2 being
set holds
{x1,x1,x1,x1,x1,x2} = {x1,x2}
theorem Th49:
for
x1,
x2,
x3 being
set holds
{x1,x1,x1,x1,x1,x2,x3} = {x1,x2,x3}
theorem Th50:
for
x1,
x2,
x3,
x4 being
set holds
{x1,x1,x1,x1,x1,x2,x3,x4} = {x1,x2,x3,x4}
theorem
for
x1 being
set holds
{x1,x1,x1,x1,x1,x1} = {x1}
theorem Th52:
for
x1,
x2 being
set holds
{x1,x1,x1,x1,x1,x1,x2} = {x1,x2}
theorem Th53:
for
x1,
x2,
x3 being
set holds
{x1,x1,x1,x1,x1,x1,x2,x3} = {x1,x2,x3}
theorem
for
x1 being
set holds
{x1,x1,x1,x1,x1,x1,x1} = {x1}
theorem Th55:
for
x1,
x2 being
set holds
{x1,x1,x1,x1,x1,x1,x1,x2} = {x1,x2}
theorem
for
x1 being
set holds
{x1,x1,x1,x1,x1,x1,x1,x1} = {x1}
theorem Th57:
for
x1,
x2,
x3 being
set holds
{x1,x2,x3} = {x1,x3,x2}
theorem Th58:
for
x1,
x2,
x3 being
set holds
{x1,x2,x3} = {x2,x1,x3}
theorem Th59:
for
x1,
x2,
x3 being
set holds
{x1,x2,x3} = {x2,x3,x1}
theorem Th60:
for
x1,
x2,
x3 being
set holds
{x1,x2,x3} = {x3,x2,x1}
theorem Th61:
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x1,x2,x4,x3}
theorem
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x1,x3,x2,x4}
theorem Th63:
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x1,x3,x4,x2}
theorem Th64:
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x1,x4,x3,x2}
theorem Th65:
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x2,x1,x3,x4}
Lm7:
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x2,x3,x1,x4}
theorem
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x2,x1,x4,x3}
theorem
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x2,x3,x1,x4} by Lm7;
theorem
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x2,x3,x4,x1}
theorem Th69:
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x2,x4,x1,x3}
theorem
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x2,x4,x3,x1}
Lm8:
for x1, x2, x3, x4 being set holds {x1,x2,x3,x4} = {x3,x2,x1,x4}
theorem
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x3,x2,x1,x4} by Lm8;
theorem
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x3,x2,x4,x1}
theorem
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x3,x4,x1,x2}
theorem Th74:
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x3,x4,x2,x1}
theorem
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x4,x2,x3,x1}
theorem
for
x1,
x2,
x3,
x4 being
set holds
{x1,x2,x3,x4} = {x4,x3,x2,x1}
Lm9:
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8,x9}
theorem
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set holds
{x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1} \/ {x2,x3,x4,x5,x6,x7,x8,x9}
theorem
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set holds
{x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2} \/ {x3,x4,x5,x6,x7,x8,x9}
theorem
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set holds
{x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3} \/ {x4,x5,x6,x7,x8,x9}
theorem
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set holds
{x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8,x9} by Lm9;
theorem
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set holds
{x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4,x5} \/ {x6,x7,x8,x9}
theorem
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set holds
{x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4,x5,x6} \/ {x7,x8,x9}
theorem
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set holds
{x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4,x5,x6,x7} \/ {x8,x9}
theorem
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9 being
set holds
{x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4,x5,x6,x7,x8} \/ {x9}
theorem
for
x1,
x2,
x3,
x4,
x5,
x6,
x7,
x8,
x9,
x10 being
set holds
{x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} = {x1,x2,x3,x4,x5,x6,x7,x8,x9} \/ {x10}
begin
theorem
for
x1,
x2,
x3 being
set holds
{x2,x1} \/ {x3,x1} = {x1,x2,x3}