begin
theorem
for
x1,
x2,
x3,
x4,
x5,
x6 being ( ( ) ( )
set ) holds
{x1 : ( ( ) ( ) set ) ,x2 : ( ( ) ( ) set ) ,x3 : ( ( ) ( ) set ) ,x4 : ( ( ) ( ) set ) ,x5 : ( ( ) ( ) set ) ,x6 : ( ( ) ( ) set ) } : ( ( ) ( non
empty V36() )
set )
= {x1 : ( ( ) ( ) set ) ,x3 : ( ( ) ( ) set ) ,x6 : ( ( ) ( ) set ) } : ( ( ) ( non
empty V36() )
set )
\/ {x2 : ( ( ) ( ) set ) ,x4 : ( ( ) ( ) set ) ,x5 : ( ( ) ( ) set ) } : ( ( ) ( non
empty V36() )
set ) : ( ( ) ( non
empty V36() )
set ) ;
theorem
for
x1,
x2,
x3,
x4,
x5,
x6 being ( ( ) ( )
set ) st
x1 : ( ( ) ( )
set ) ,
x2 : ( ( ) ( )
set ) ,
x3 : ( ( ) ( )
set ) ,
x4 : ( ( ) ( )
set ) ,
x5 : ( ( ) ( )
set ) ,
x6 : ( ( ) ( )
set )
are_mutually_different holds
card {x1 : ( ( ) ( ) set ) ,x2 : ( ( ) ( ) set ) ,x3 : ( ( ) ( ) set ) ,x4 : ( ( ) ( ) set ) ,x5 : ( ( ) ( ) set ) ,x6 : ( ( ) ( ) set ) } : ( ( ) ( non
empty V36() )
set ) : ( ( ) (
natural complex real ext-real V128()
V129()
V130()
V131()
V132()
V133()
integer non
irrational )
Element of
omega : ( ( ) (
V128()
V129()
V130()
V131()
V132()
V133()
V134() )
set ) )
= 6 : ( ( ) ( non
empty natural complex real ext-real positive non
negative V128()
V129()
V130()
V131()
V132()
V133()
integer non
irrational )
Element of
NAT : ( ( ) (
V128()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
bool REAL : ( ( ) (
V128()
V129()
V130()
V134() )
set ) : ( ( ) ( non
empty )
set ) ) ) ;
theorem
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being ( ( ) ( )
set ) st
x1 : ( ( ) ( )
set ) ,
x2 : ( ( ) ( )
set ) ,
x3 : ( ( ) ( )
set ) ,
x4 : ( ( ) ( )
set ) ,
x5 : ( ( ) ( )
set ) ,
x6 : ( ( ) ( )
set ) ,
x7 : ( ( ) ( )
set )
are_mutually_different holds
card {x1 : ( ( ) ( ) set ) ,x2 : ( ( ) ( ) set ) ,x3 : ( ( ) ( ) set ) ,x4 : ( ( ) ( ) set ) ,x5 : ( ( ) ( ) set ) ,x6 : ( ( ) ( ) set ) ,x7 : ( ( ) ( ) set ) } : ( ( ) ( non
empty V36() )
set ) : ( ( ) (
natural complex real ext-real V128()
V129()
V130()
V131()
V132()
V133()
integer non
irrational )
Element of
omega : ( ( ) (
V128()
V129()
V130()
V131()
V132()
V133()
V134() )
set ) )
= 7 : ( ( ) ( non
empty natural complex real ext-real positive non
negative V128()
V129()
V130()
V131()
V132()
V133()
integer non
irrational )
Element of
NAT : ( ( ) (
V128()
V129()
V130()
V131()
V132()
V133()
V134() )
Element of
bool REAL : ( ( ) (
V128()
V129()
V130()
V134() )
set ) : ( ( ) ( non
empty )
set ) ) ) ;
theorem
for
x1,
x2,
x3,
x4,
x5,
x6 being ( ( ) ( )
set ) st
{x1 : ( ( ) ( ) set ) ,x2 : ( ( ) ( ) set ) ,x3 : ( ( ) ( ) set ) } : ( ( ) ( non
empty V36() )
set )
misses {x4 : ( ( ) ( ) set ) ,x5 : ( ( ) ( ) set ) ,x6 : ( ( ) ( ) set ) } : ( ( ) ( non
empty V36() )
set ) holds
(
x1 : ( ( ) ( )
set )
<> x4 : ( ( ) ( )
set ) &
x1 : ( ( ) ( )
set )
<> x5 : ( ( ) ( )
set ) &
x1 : ( ( ) ( )
set )
<> x6 : ( ( ) ( )
set ) &
x2 : ( ( ) ( )
set )
<> x4 : ( ( ) ( )
set ) &
x2 : ( ( ) ( )
set )
<> x5 : ( ( ) ( )
set ) &
x2 : ( ( ) ( )
set )
<> x6 : ( ( ) ( )
set ) &
x3 : ( ( ) ( )
set )
<> x4 : ( ( ) ( )
set ) &
x3 : ( ( ) ( )
set )
<> x5 : ( ( ) ( )
set ) &
x3 : ( ( ) ( )
set )
<> x6 : ( ( ) ( )
set ) ) ;
theorem
for
x1,
x2,
x3,
x4,
x5,
x6 being ( ( ) ( )
set ) st
x1 : ( ( ) ( )
set ) ,
x2 : ( ( ) ( )
set ) ,
x3 : ( ( ) ( )
set )
are_mutually_different &
x4 : ( ( ) ( )
set ) ,
x5 : ( ( ) ( )
set ) ,
x6 : ( ( ) ( )
set )
are_mutually_different &
{x1 : ( ( ) ( ) set ) ,x2 : ( ( ) ( ) set ) ,x3 : ( ( ) ( ) set ) } : ( ( ) ( non
empty V36() )
set )
misses {x4 : ( ( ) ( ) set ) ,x5 : ( ( ) ( ) set ) ,x6 : ( ( ) ( ) set ) } : ( ( ) ( non
empty V36() )
set ) holds
x1 : ( ( ) ( )
set ) ,
x2 : ( ( ) ( )
set ) ,
x3 : ( ( ) ( )
set ) ,
x4 : ( ( ) ( )
set ) ,
x5 : ( ( ) ( )
set ) ,
x6 : ( ( ) ( )
set )
are_mutually_different ;
theorem
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being ( ( ) ( )
set ) st
x1 : ( ( ) ( )
set ) ,
x2 : ( ( ) ( )
set ) ,
x3 : ( ( ) ( )
set ) ,
x4 : ( ( ) ( )
set ) ,
x5 : ( ( ) ( )
set ) ,
x6 : ( ( ) ( )
set )
are_mutually_different &
{x1 : ( ( ) ( ) set ) ,x2 : ( ( ) ( ) set ) ,x3 : ( ( ) ( ) set ) ,x4 : ( ( ) ( ) set ) ,x5 : ( ( ) ( ) set ) ,x6 : ( ( ) ( ) set ) } : ( ( ) ( non
empty V36() )
set )
misses {x7 : ( ( ) ( ) set ) } : ( ( ) ( non
empty V36() )
set ) holds
x1 : ( ( ) ( )
set ) ,
x2 : ( ( ) ( )
set ) ,
x3 : ( ( ) ( )
set ) ,
x4 : ( ( ) ( )
set ) ,
x5 : ( ( ) ( )
set ) ,
x6 : ( ( ) ( )
set ) ,
x7 : ( ( ) ( )
set )
are_mutually_different ;
theorem
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being ( ( ) ( )
set ) st
x1 : ( ( ) ( )
set ) ,
x2 : ( ( ) ( )
set ) ,
x3 : ( ( ) ( )
set ) ,
x4 : ( ( ) ( )
set ) ,
x5 : ( ( ) ( )
set ) ,
x6 : ( ( ) ( )
set ) ,
x7 : ( ( ) ( )
set )
are_mutually_different holds
x7 : ( ( ) ( )
set ) ,
x1 : ( ( ) ( )
set ) ,
x2 : ( ( ) ( )
set ) ,
x3 : ( ( ) ( )
set ) ,
x4 : ( ( ) ( )
set ) ,
x5 : ( ( ) ( )
set ) ,
x6 : ( ( ) ( )
set )
are_mutually_different ;
theorem
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being ( ( ) ( )
set ) st
x1 : ( ( ) ( )
set ) ,
x2 : ( ( ) ( )
set ) ,
x3 : ( ( ) ( )
set ) ,
x4 : ( ( ) ( )
set ) ,
x5 : ( ( ) ( )
set ) ,
x6 : ( ( ) ( )
set ) ,
x7 : ( ( ) ( )
set )
are_mutually_different holds
x1 : ( ( ) ( )
set ) ,
x2 : ( ( ) ( )
set ) ,
x5 : ( ( ) ( )
set ) ,
x3 : ( ( ) ( )
set ) ,
x6 : ( ( ) ( )
set ) ,
x7 : ( ( ) ( )
set ) ,
x4 : ( ( ) ( )
set )
are_mutually_different ;
begin
begin
begin
begin