begin
theorem
canceled;
theorem Th2:
theorem
for
x1,
x2,
x3,
x4,
x5,
x6 being
set holds
{x1,x2,x3,x4,x5,x6} = {x1,x3,x6} \/ {x2,x4,x5}
definition
canceled;
canceled;
end;
:: deftheorem BORSUK_5:def 1 :
canceled;
:: deftheorem BORSUK_5:def 2 :
canceled;
theorem Th4:
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 Th6:
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 arcwise_connected
begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th28:
theorem Th29:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th34:
theorem Th35:
theorem Th36:
begin
:: deftheorem defines IRRAT BORSUK_5:def 3 :
:: deftheorem defines RAT BORSUK_5:def 4 :
:: deftheorem defines IRRAT BORSUK_5:def 5 :
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem
canceled;
theorem Th47:
theorem
canceled;
theorem
canceled;
theorem Th50:
theorem Th51:
Lm2:
for A being Subset of
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
for a, b being real number st a < b & A = IRRAT a,b holds
( a in Cl A & b in Cl A )
theorem Th52:
theorem Th53:
theorem Th54:
theorem Th55:
theorem Th56:
theorem Th57:
begin
theorem Th58:
theorem Th59:
theorem
theorem Th61:
theorem Th62:
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
theorem Th63:
theorem
canceled;
theorem Th65:
theorem Th66:
theorem Th67:
theorem Th68:
theorem
canceled;
theorem
canceled;
theorem Th71:
theorem
theorem
theorem Th74:
theorem Th75:
theorem
theorem Th77:
theorem
theorem Th79:
theorem
theorem Th81:
theorem
theorem
canceled;
theorem Th84:
Lm7:
for a, b being real number st b <= a holds
RAT a,b = {}
Lm8:
for a, b being real number st b <= a holds
REAL = ].-infty ,a.] \/ [.b,+infty .[
theorem Th85:
theorem
canceled;
theorem
canceled;
theorem Th88:
theorem
theorem
Lm9:
((IRRAT 2,4) \/ {4}) \/ {5} c= ].1,+infty .[
Lm10:
].1,+infty .[ c= [.1,+infty .[
by XXREAL_1:45;
Lm11:
].-infty ,1.[ /\ (((].-infty ,2.] \/ (IRRAT 2,4)) \/ {4}) \/ {5}) = ].-infty ,1.[
Lm12:
].1,+infty .[ /\ (((].-infty ,2.] \/ (IRRAT 2,4)) \/ {4}) \/ {5}) = ((].1,2.] \/ (IRRAT 2,4)) \/ {4}) \/ {5}
theorem
canceled;
theorem
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem Th97:
theorem
canceled;
theorem
canceled;
theorem Th100:
theorem
theorem
theorem
theorem
theorem
theorem
begin
theorem Th107:
theorem Th108:
theorem Th109:
theorem Th110:
theorem Th111:
theorem Th112:
theorem