begin
theorem
for
x1,
x2,
x3,
x4,
x5,
x6 being
set holds
{x1,x2,x3,x4,x5,x6} = {x1,x3,x6} \/ {x2,x4,x5}
theorem Th3:
for
x1,
x2,
x3,
x4,
x5,
x6 being
set st
x1,
x2,
x3,
x4,
x5,
x6 are_mutually_different holds
card {x1,x2,x3,x4,x5,x6} = 6
theorem
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set st
x1,
x2,
x3,
x4,
x5,
x6,
x7 are_mutually_different holds
card {x1,x2,x3,x4,x5,x6,x7} = 7
theorem Th5:
for
x1,
x2,
x3,
x4,
x5,
x6 being
set st
{x1,x2,x3} misses {x4,x5,x6} holds
(
x1 <> x4 &
x1 <> x5 &
x1 <> x6 &
x2 <> x4 &
x2 <> x5 &
x2 <> x6 &
x3 <> x4 &
x3 <> x5 &
x3 <> x6 )
theorem
for
x1,
x2,
x3,
x4,
x5,
x6 being
set st
x1,
x2,
x3 are_mutually_different &
x4,
x5,
x6 are_mutually_different &
{x1,x2,x3} misses {x4,x5,x6} holds
x1,
x2,
x3,
x4,
x5,
x6 are_mutually_different
theorem
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set st
x1,
x2,
x3,
x4,
x5,
x6 are_mutually_different &
{x1,x2,x3,x4,x5,x6} misses {x7} holds
x1,
x2,
x3,
x4,
x5,
x6,
x7 are_mutually_different
theorem
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set st
x1,
x2,
x3,
x4,
x5,
x6,
x7 are_mutually_different holds
x7,
x1,
x2,
x3,
x4,
x5,
x6 are_mutually_different
theorem
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set st
x1,
x2,
x3,
x4,
x5,
x6,
x7 are_mutually_different holds
x1,
x2,
x5,
x3,
x6,
x7,
x4 are_mutually_different
Lm1:
R^1 is pathwise_connected
begin
begin
Lm2:
for A being Subset of R^1
for a, b being real number st a < b & A = RAT (a,b) holds
( a in Cl A & b in Cl A )
Lm3:
for A being Subset of R^1
for a, b being real number st a < b & A = IRRAT (a,b) holds
( a in Cl A & b in Cl A )
begin
Lm4:
for a being real number holds ].-infty,a.] is closed
Lm5:
for a being real number holds [.a,+infty.[ is closed
Lm6:
for a, b being ext-real number holds ].a,b.[ is open
Lm7:
((IRRAT (2,4)) \/ {4}) \/ {5} c= ].1,+infty.[
Lm8:
].1,+infty.[ c= [.1,+infty.[
by XXREAL_1:45;
Lm9:
].-infty,1.[ /\ (((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5}) = ].-infty,1.[
Lm10:
].1,+infty.[ /\ (((].-infty,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5}) = ((].1,2.] \/ (IRRAT (2,4))) \/ {4}) \/ {5}
begin