environ
vocabularies HIDDEN, NUMBERS, TARSKI, XBOOLE_0, ZFMISC_1, CARD_1, ARYTM_3, TOPMETR, BORSUK_2, PRE_TOPC, XXREAL_0, XXREAL_1, SUBSET_1, RELAT_1, STRUCT_0, TREAL_1, VALUED_1, FUNCT_1, BORSUK_1, ORDINAL2, GRAPH_1, ARYTM_1, RELAT_2, XREAL_0, CONNSP_1, REAL_1, LIMFUNC1, METRIC_1, COMPLEX1, RAT_1, POWER, IRRAT_1, INT_1, XCMPLX_0, RCOMP_1, PCOMPS_1, XXREAL_2, SEQ_4, SETFAM_1, BORSUK_5, MEASURE5;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XREAL_0, ENUMSET1, FUNCT_1, FUNCT_2, XXREAL_2, MEASURE6, STRUCT_0, INT_1, COMPLEX1, PRE_TOPC, TOPS_2, COMPTS_1, RCOMP_1, SEQ_4, TREAL_1, CONNSP_1, BORSUK_2, TOPMETR, LIMFUNC1, IRRAT_1, RAT_1, MEASURE5, METRIC_1, PCOMPS_1, XXREAL_0;
definitions XBOOLE_0, TARSKI, BORSUK_2, TOPS_2;
theorems BORSUK_1, PRE_TOPC, COMPTS_1, TARSKI, TOPMETR, RCOMP_1, CONNSP_1, ZFMISC_1, JORDAN5A, XREAL_0, TREAL_1, XBOOLE_0, XBOOLE_1, SEQ_4, INTEGRA1, FUNCT_2, TOPS_1, BORSUK_4, BORSUK_2, ENUMSET1, RAT_1, METRIC_1, ABSVALUE, XCMPLX_1, CARD_2, INT_1, YELLOW_8, IRRAT_1, NUMBERS, XREAL_1, SUBSET_1, GOBOARD6, XXREAL_0, XXREAL_1, XXREAL_2, MEASURE5;
schemes ;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, XXREAL_0, XREAL_0, INT_1, RAT_1, MEMBERED, STRUCT_0, PRE_TOPC, TOPS_1, METRIC_1, TOPMETR, BORSUK_2, TOPREAL6, FCONT_3, RCOMP_1, MEASURE5, ORDINAL1;
constructors HIDDEN, COMPLEX1, PROB_1, LIMFUNC1, POWER, CONNSP_1, TOPS_2, COMPTS_1, TREAL_1, MEASURE6, BORSUK_2, INTEGRA1, SEQ_4, BINOP_2, PCOMPS_1;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities SUBSET_1, STRUCT_0, LIMFUNC1, PROB_1;
expansions TARSKI, BORSUK_2, TOPS_2;
theorem
for
x1,
x2,
x3,
x4,
x5,
x6 being
set holds
{x1,x2,x3,x4,x5,x6} = {x1,x3,x6} \/ {x2,x4,x5}
theorem Th2:
for
x1,
x2,
x3,
x4,
x5,
x6 being
set st
x1,
x2,
x3,
x4,
x5,
x6 are_mutually_distinct 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_distinct holds
card {x1,x2,x3,x4,x5,x6,x7} = 7
theorem Th4:
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_distinct &
x4,
x5,
x6 are_mutually_distinct &
{x1,x2,x3} misses {x4,x5,x6} holds
x1,
x2,
x3,
x4,
x5,
x6 are_mutually_distinct
theorem
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set st
x1,
x2,
x3,
x4,
x5,
x6 are_mutually_distinct &
{x1,x2,x3,x4,x5,x6} misses {x7} holds
x1,
x2,
x3,
x4,
x5,
x6,
x7 are_mutually_distinct
theorem
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set st
x1,
x2,
x3,
x4,
x5,
x6,
x7 are_mutually_distinct holds
x7,
x1,
x2,
x3,
x4,
x5,
x6 are_mutually_distinct
theorem
for
x1,
x2,
x3,
x4,
x5,
x6,
x7 being
set st
x1,
x2,
x3,
x4,
x5,
x6,
x7 are_mutually_distinct holds
x1,
x2,
x5,
x3,
x6,
x7,
x4 are_mutually_distinct
Lm1:
R^1 is pathwise_connected
theorem Th25:
for
a,
b being
Real st
a < b holds
ex
p1,
p2 being
Rational st
(
a < p1 &
p1 < p2 &
p2 < b )
Lm2:
for A being Subset of R^1
for a, b being Real 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 st a < b & A = IRRAT (a,b) holds
( a in Cl A & b in Cl A )
Lm4:
for a being Real holds ].-infty,a.] is closed
Lm5:
for a being Real holds [.a,+infty.[ is closed
Lm6:
for a, b being ExtReal 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}