:: BORSUK_4 semantic presentation

registration
cluster -> non trivial Element of K18(the carrier of (TOP-REAL 2));
coherence
for b1 being Simple_closed_curve holds
not b1 is trivial
proof
let c1 be Simple_closed_curve;
ex b1, b2 being Point of (TOP-REAL 2) st
( b1 <> b2 & b1 in c1 & b2 in c1 ) by TOPREAL2:5;
hence not c1 is trivial by REALSET1:14;
end;
end;

theorem Th1: :: BORSUK_4:1
for b1 being non empty set
for b2, b3 being non empty Subset of b1 holds
not ( b2 c< b3 & ( for b4 being Element of b1 holds
not ( b4 in b3 & b2 c= b3 \ {b4} ) ) )
proof
let c1 be non empty set ;
let c2, c3 be non empty Subset of c1;
assume E2: c2 c< c3 ;
then c3 \ c2 <> {} by XBOOLE_1:105;
then consider c4 being set such that
E3: c4 in c3 \ c2 by XBOOLE_0:def 1;
E4: ( c4 in c3 & not c4 in c2 ) by E3, XBOOLE_0:def 4;
reconsider c5 = c4 as Element of c1 by E3;
take c5 ;
c2 c= c3 by E2, XBOOLE_0:def 8;
hence ( c5 in c3 & c2 c= c3 \ {c5} ) by E4, ZFMISC_1:40;
end;

theorem Th2: :: BORSUK_4:2
for b1 being non empty set
for b2 being non empty Subset of b1 holds
( b2 is trivial iff ex b3 being Element of b1 st b2 = {b3} )
proof
let c1 be non empty set ;
let c2 be non empty Subset of c1;
hereby
assume c2 is trivial ;
then consider c3 being Element of c2 such that
E3: c2 = {c3} by TEX_2:def 1;
thus ex b1 being Element of c1 st c2 = {b1} by E3;
end;
given c3 being Element of c1 such that E3: c2 = {c3} ;
thus c2 is trivial by E3;
end;

registration
let c1 be non trivial 1-sorted ;
cluster non trivial Element of K18(the carrier of a1);
existence
not for b1 being Subset of c1 holds b1 is trivial
proof
consider c2, c3 being Element of c1 such that
E3: c2 <> c3 by REALSET2:def 7;
take c4 = {c2,c3};
( c2 in c4 & c3 in c4 ) by TARSKI:def 2;
hence not c4 is trivial by E3, REALSET1:15;
end;
end;

theorem Th3: :: BORSUK_4:3
for b1 being non trivial set
for b2 being set holds
not for b3 being Element of b1 holds not b3 <> b2
proof
let c1 be non trivial set ;
let c2 be set ;
not c1 \ {c2} is empty by REALSET1:4;
then consider c3 being set such that
E4: c3 in c1 \ {c2} by XBOOLE_0:def 1;
reconsider c4 = c3 as Element of c1 by E4;
take c4 ;
thus c4 <> c2 by E4, ZFMISC_1:64;
end;

registration
let c1 be non trivial set ;
cluster non trivial Element of K18(a1);
existence
not for b1 being Subset of c1 holds b1 is trivial
proof
take [#] c1 ;
thus not [#] c1 is trivial ;
end;
end;

theorem Th4: :: BORSUK_4:4
for b1 being non trivial set
for b2 being non trivial Subset of b1
for b3 being set holds
ex b4 being Element of b1 st
( b4 in b2 & b4 <> b3 )
proof
let c1 be non trivial set ;
let c2 be non trivial Subset of c1;
let c3 be set ;
set c4 = c3;
not c2 \ {c3} is empty by REALSET1:4;
then consider c5 being set such that
E5: c5 in c2 \ {c3} by XBOOLE_0:def 1;
c5 in c2 by E5, XBOOLE_0:def 4;
then reconsider c6 = c5 as Element of c1 ;
take c6 ;
thus ( c6 in c2 & c6 <> c3 ) by E5, ZFMISC_1:64;
end;

theorem Th5: :: BORSUK_4:5
for b1, b2 being Function
for b3 being set holds
( b1 is one-to-one & b2 is one-to-one & (dom b1) /\ (dom b2) = {b3} & (rng b1) /\ (rng b2) = {(b1 . b3)} implies b1 +* b2 is one-to-one )
proof
let c1, c2 be Function;
let c3 be set ;
assume that
E6: c1 is one-to-one and
E7: c2 is one-to-one and
E8: (dom c1) /\ (dom c2) = {c3} and
E9: (rng c1) /\ (rng c2) = {(c1 . c3)} ;
for b1, b2 being set holds
not ( b1 in dom c2 & b2 in (dom c1) \ (dom c2) & not c2 . b1 <> c1 . b2 )
proof
let c4, c5 be set ;
assume E10: ( c4 in dom c2 & c5 in (dom c1) \ (dom c2) ) ;
then E11: c2 . c4 in rng c2 by FUNCT_1:12;
E12: c1 . c5 in rng c1 by E10, FUNCT_1:12;
( {c3} c= dom c1 & {c3} c= dom c2 ) by E8, XBOOLE_1:17;
then E13: ( c3 in dom c1 & c3 in dom c2 ) by ZFMISC_1:37;
assume c2 . c4 = c1 . c5 ;
then c1 . c5 in (rng c1) /\ (rng c2) by E11, E12, XBOOLE_0:def 3;
then c1 . c5 = c1 . c3 by E9, TARSKI:def 1;
then c5 = c3 by E6, E10, E13, FUNCT_1:def 8;
then dom c2 meets (dom c1) \ (dom c2) by E10, E13, XBOOLE_0:3;
hence not verum by XBOOLE_1:79;
end;
hence c1 +* c2 is one-to-one by E6, E7, TOPMETR2:2;
end;

theorem Th6: :: BORSUK_4:6
for b1, b2 being Function
for b3 being set holds
( b1 is one-to-one & b2 is one-to-one & (dom b1) /\ (dom b2) = {b3} & (rng b1) /\ (rng b2) = {(b1 . b3)} & b1 . b3 = b2 . b3 implies (b1 +* b2) " = (b1 " ) +* (b2 " ) )
proof
let c1, c2 be Function;
let c3 be set ;
assume that
E7: c1 is one-to-one and
E8: c2 is one-to-one and
E9: (dom c1) /\ (dom c2) = {c3} and
E10: (rng c1) /\ (rng c2) = {(c1 . c3)} and
E11: c1 . c3 = c2 . c3 ;
set c4 = (c1 " ) +* (c2 " );
set c5 = c1 +* c2;
for b1 being set holds
( b1 in (dom c1) /\ (dom c2) implies c1 . b1 = c2 . b1 )
proof
let c6 be set ;
assume c6 in (dom c1) /\ (dom c2) ;
then c6 = c3 by E9, TARSKI:def 1;
hence c1 . c6 = c2 . c6 by E11;
end;
then E12: c1 tolerates c2 by PARTFUN1:def 6;
E13: ( dom (c1 " ) = rng c1 & dom (c2 " ) = rng c2 ) by E7, E8, FUNCT_1:55;
for b1 being set holds
( b1 in (dom (c1 " )) /\ (dom (c2 " )) implies (c1 " ) . b1 = (c2 " ) . b1 )
proof
let c6 be set ;
assume E14: c6 in (dom (c1 " )) /\ (dom (c2 " )) ;
{c3} c= dom c1 by E9, XBOOLE_1:17;
then E15: c3 in dom c1 by ZFMISC_1:37;
{c3} c= dom c2 by E9, XBOOLE_1:17;
then E16: c3 in dom c2 by ZFMISC_1:37;
c6 = c1 . c3 by E10, E13, E14, TARSKI:def 1;
then E17: c3 = (c1 " ) . c6 by E7, E15, FUNCT_1:54;
c6 = c2 . c3 by E10, E11, E13, E14, TARSKI:def 1;
hence (c1 " ) . c6 = (c2 " ) . c6 by E8, E16, E17, FUNCT_1:54;
end;
then E14: c1 " tolerates c2 " by PARTFUN1:def 6;
E15: c1 +* c2 is one-to-one by E7, E8, E9, E10, Th5;
E16: rng (c1 +* c2) = (rng c1) \/ (rng c2) by E12, FRECHET:39;
dom ((c1 " ) +* (c2 " )) = (dom (c1 " )) \/ (dom (c2 " )) by FUNCT_4:def 1
.= (rng c1) \/ (dom (c2 " )) by E7, FUNCT_1:55
.= (rng c1) \/ (rng c2) by E8, FUNCT_1:55 ;
then E17: dom ((c1 " ) +* (c2 " )) = rng (c1 +* c2) by E12, FRECHET:39;
E18: dom (c1 +* c2) = (dom c1) \/ (dom c2) by FUNCT_4:def 1;
then E19: dom c1 c= dom (c1 +* c2) by XBOOLE_1:7;
E20: dom c2 c= dom (c1 +* c2) by E18, XBOOLE_1:7;
for b1, b2 being set holds
( ( b1 in rng (c1 +* c2) & b2 = ((c1 " ) +* (c2 " )) . b1 implies ( b2 in dom (c1 +* c2) & b1 = (c1 +* c2) . b2 ) ) & ( b2 in dom (c1 +* c2) & b1 = (c1 +* c2) . b2 implies ( b1 in rng (c1 +* c2) & b2 = ((c1 " ) +* (c2 " )) . b1 ) ) )
proof
let c6, c7 be set ;
hereby
assume E21: ( c6 in rng (c1 +* c2) & c7 = ((c1 " ) +* (c2 " )) . c6 ) ;
per cases ( c6 in dom (c1 " ) or c6 in dom (c2 " ) ) by E17, E21, FUNCT_4:13;
suppose E22: c6 in dom (c1 " ) ;
then E23: c6 in rng c1 by E7, FUNCT_1:55;
c7 = (c1 " ) . c6 by E14, E21, E22, FUNCT_4:16;
then ( c7 in dom c1 & c6 = c1 . c7 ) by E7, E23, FUNCT_1:54;
hence ( c7 in dom (c1 +* c2) & c6 = (c1 +* c2) . c7 ) by E12, E19, FUNCT_4:16;
end;
suppose E22: c6 in dom (c2 " ) ;
then E23: c6 in rng c2 by E8, FUNCT_1:55;
c7 = (c2 " ) . c6 by E21, E22, FUNCT_4:14;
then ( c7 in dom c2 & c6 = c2 . c7 ) by E8, E23, FUNCT_1:54;
hence ( c7 in dom (c1 +* c2) & c6 = (c1 +* c2) . c7 ) by E20, FUNCT_4:14;
end;
end;
end;
assume E21: ( c7 in dom (c1 +* c2) & c6 = (c1 +* c2) . c7 ) ;
per cases ( c7 in dom c1 or c7 in dom c2 ) by E21, FUNCT_4:13;
suppose E22: c7 in dom c1 ;
then E23: c6 = c1 . c7 by E12, E21, FUNCT_4:16;
then E24: c7 = (c1 " ) . c6 by E7, E22, FUNCT_1:54;
E25: c6 in rng c1 by E22, E23, FUNCT_1:12;
rng (c1 +* c2) = (rng c1) \/ (rng c2) by E12, FRECHET:39;
then E26: rng c1 c= rng (c1 +* c2) by XBOOLE_1:7;
c6 in dom (c1 " ) by E7, E25, FUNCT_1:55;
hence ( c6 in rng (c1 +* c2) & c7 = ((c1 " ) +* (c2 " )) . c6 ) by E14, E24, E25, E26, FUNCT_4:16;
end;
suppose E22: c7 in dom c2 ;
then E23: c6 = c2 . c7 by E21, FUNCT_4:14;
then E24: c7 = (c2 " ) . c6 by E8, E22, FUNCT_1:54;
E25: c6 in rng c2 by E22, E23, FUNCT_1:12;
E26: rng c2 c= rng (c1 +* c2) by E16, XBOOLE_1:7;
c6 in dom (c2 " ) by E8, E25, FUNCT_1:55;
hence ( c6 in rng (c1 +* c2) & c7 = ((c1 " ) +* (c2 " )) . c6 ) by E24, E25, E26, FUNCT_4:14;
end;
end;
end;
hence (c1 +* c2) " = (c1 " ) +* (c2 " ) by E15, E17, FUNCT_1:54;
end;

theorem Th7: :: BORSUK_4:7
for b1 being Nat
for b2 being Subset of (TOP-REAL b1)
for b3, b4 being Point of (TOP-REAL b1) holds
not ( b2 is_an_arc_of b3,b4 & b2 \ {b3} is empty )
proof
let c1 be Nat;
let c2 be Subset of (TOP-REAL c1);
let c3, c4 be Point of (TOP-REAL c1);
assume c2 is_an_arc_of c3,c4 ;
then E8: c2 \ {c3,c4} <> {} by JORDAN6:56;
{c3} c= {c3,c4} by ZFMISC_1:12;
then c2 \ {c3,c4} c= c2 \ {c3} by XBOOLE_1:34;
hence not c2 \ {c3} is empty by E8, XBOOLE_1:3;
end;

theorem Th8: :: BORSUK_4:8
for b1 being Nat
for b2, b3 being Point of (TOP-REAL b1) holds LSeg b2,b3 is convex
proof
let c1 be Nat;
let c2, c3 be Point of (TOP-REAL c1);
set c4 = LSeg c2,c3;
let c5, c6 be Point of (TOP-REAL c1); :: according to JORDAN1:def 1
assume ( c5 in LSeg c2,c3 & c6 in LSeg c2,c3 ) ;
hence LSeg c5,c6 c= LSeg c2,c3 by TOPREAL1:12;
end;

theorem Th9: :: BORSUK_4:9
for b1, b2, b3, b4 being real number holds
( b1 <= b2 & b1 < b3 & 0 <= b4 & b4 <= 1 implies b1 <= ((1 - b4) * b2) + (b4 * b3) )
proof
let c1, c2, c3, c4 be real number ;
assume E8: ( c1 <= c2 & c1 < c3 & 0 <= c4 & c4 <= 1 ) ;
now
per cases not ( not c4 = 0 & not c4 = 1 & not ( not c4 = 0 & not c4 = 1 ) ) ;
suppose c4 = 0 ;
hence c1 <= ((1 - c4) * c2) + (c4 * c3) by E8;
end;
suppose c4 = 1 ;
hence c1 <= ((1 - c4) * c2) + (c4 * c3) by E8;
end;
suppose E9: ( not c4 = 0 & not c4 = 1 ) ;
then E10: ( c4 > 0 & c4 < 1 ) by E8, REAL_1:def 5;
E11: c4 * c1 < c4 * c3 by E8, E9, XREAL_1:70;
1 - c4 > 0 by E10, XREAL_1:52;
then E12: (1 - c4) * c1 <= (1 - c4) * c2 by E8, XREAL_1:66;
((1 - c4) * c1) + (c4 * c1) = 1 * c1 ;
hence c1 <= ((1 - c4) * c2) + (c4 * c3) by E11, E12, XREAL_1:10;
end;
end;
end;
hence c1 <= ((1 - c4) * c2) + (c4 * c3) ;
end;

theorem Th10: :: BORSUK_4:10
for b1 being set
for b2, b3 being real number holds
not ( b1 in [.b2,b3.] & not b1 in ].b2,b3.[ & not b1 = b2 & not b1 = b3 )
proof
let c1 be set ;
let c2, c3 be real number ;
assume E9: c1 in [.c2,c3.] ;
then c2 <= c3 by RCOMP_1:13;
then c1 in ].c2,c3.[ \/ {c2,c3} by E9, RCOMP_1:11;
then ( c1 in ].c2,c3.[ or c1 in {c2,c3} ) by XBOOLE_0:def 2;
hence not ( not c1 in ].c2,c3.[ & not c1 = c2 & not c1 = c3 ) by TARSKI:def 2;
end;

theorem Th11: :: BORSUK_4:11
for b1, b2, b3, b4 being real number holds
not ( ].b1,b2.[ meets [.b3,b4.] & not b2 > b3 )
proof
let c1, c2, c3, c4 be real number ;
assume E10: ].c1,c2.[ meets [.c3,c4.] ;
assume E11: c2 <= c3 ;
consider c5 being set such that
E12: ( c5 in ].c1,c2.[ & c5 in [.c3,c4.] ) by E10, XBOOLE_0:3;
c5 in { b1 where B is Real : ( c1 < b1 & b1 < c2 ) } by E12, RCOMP_1:def 2;
then consider c6 being Real such that
E13: ( c6 = c5 & c1 < c6 & c6 < c2 ) ;
c5 in { b1 where B is Real : ( c3 <= b1 & b1 <= c4 ) } by E12, RCOMP_1:def 1;
then consider c7 being Real such that
E14: ( c7 = c5 & c3 <= c7 & c7 <= c4 ) ;
thus not verum by E11, E13, E14, XXREAL_0:2;
end;

theorem Th12: :: BORSUK_4:12
for b1, b2, b3, b4 being real number holds
( b2 <= b3 implies [.b1,b2.] misses ].b3,b4.[ )
proof
let c1, c2, c3, c4 be real number ;
assume E11: c2 <= c3 ;
assume [.c1,c2.] meets ].c3,c4.[ ;
then consider c5 being set such that
E12: ( c5 in [.c1,c2.] & c5 in ].c3,c4.[ ) by XBOOLE_0:3;
c5 in { b1 where B is Real : ( c1 <= b1 & b1 <= c2 ) } by E12, RCOMP_1:def 1;
then consider c6 being Real such that
E13: ( c6 = c5 & c1 <= c6 & c6 <= c2 ) ;
c5 in { b1 where B is Real : ( c3 < b1 & b1 < c4 ) } by E12, RCOMP_1:def 2;
then consider c7 being Real such that
E14: ( c7 = c5 & c3 < c7 & c7 < c4 ) ;
thus not verum by E11, E13, E14, XXREAL_0:2;
end;

theorem Th13: :: BORSUK_4:13
for b1, b2, b3, b4 being real number holds
( b2 <= b3 implies ].b1,b2.[ misses [.b3,b4.] )
proof
let c1, c2, c3, c4 be real number ;
assume E12: c2 <= c3 ;
assume ].c1,c2.[ meets [.c3,c4.] ;
then consider c5 being set such that
E13: ( c5 in ].c1,c2.[ & c5 in [.c3,c4.] ) by XBOOLE_0:3;
c5 in { b1 where B is Real : ( c1 < b1 & b1 < c2 ) } by E13, RCOMP_1:def 2;
then consider c6 being Real such that
E14: ( c6 = c5 & c1 < c6 & c6 < c2 ) ;
c5 in { b1 where B is Real : ( c3 <= b1 & b1 <= c4 ) } by E13, RCOMP_1:def 1;
then consider c7 being Real such that
E15: ( c7 = c5 & c3 <= c7 & c7 <= c4 ) ;
thus not verum by E12, E14, E15, XXREAL_0:2;
end;

theorem Th14: :: BORSUK_4:14
for b1, b2, b3, b4 being real number holds
( b1 <= b2 & [.b1,b2.] c= [.b3,b4.] implies ( b3 <= b1 & b2 <= b4 ) )
proof
let c1, c2, c3, c4 be real number ;
assume E12: c1 <= c2 ;
assume E13: [.c1,c2.] c= [.c3,c4.] ;
E14: c1 in [.c1,c2.] by E12, RCOMP_1:15;
c2 in [.c1,c2.] by E12, RCOMP_1:15;
hence ( c3 <= c1 & c2 <= c4 ) by E13, E14, RCOMP_1:48;
end;

theorem Th15: :: BORSUK_4:15
for b1, b2, b3, b4 being real number holds
( b1 < b2 & ].b1,b2.[ c= [.b3,b4.] implies ( b3 <= b1 & b2 <= b4 ) )
proof
let c1, c2, c3, c4 be real number ;
assume E13: ( c1 < c2 & ].c1,c2.[ c= [.c3,c4.] ) ;
then ].c1,c2.[ <> {} by RCOMP_1:15;
then E14: ].c1,c2.[ meets [.c3,c4.] by E13, XBOOLE_1:69;
assume E15: not ( not c3 > c1 & not c2 > c4 ) ;
per cases not ( not c1 < c3 & not c4 < c2 ) by E15;
suppose c1 < c3 ;
then consider c5 being real number such that
E16: ( c1 < c5 & c5 < c3 ) by XREAL_1:7;
c2 > c3 by E14, Th11;
then c5 < c2 by E16, XXREAL_0:2;
then c5 in ].c1,c2.[ by E16, RCOMP_1:47;
hence not verum by E13, E16, RCOMP_1:48;
end;
suppose E16: c4 < c2 ;
set c5 = max c1,c4;
max c1,c4 < c2 by E13, E16, RCOMP_2:2;
then consider c6 being real number such that
E17: ( max c1,c4 < c6 & c6 < c2 ) by XREAL_1:7;
E18: ( c1 <= max c1,c4 & c4 <= max c1,c4 ) by XXREAL_0:25;
then E19: c4 < c6 by E17, XXREAL_0:2;
c1 < c6 by E17, E18, XXREAL_0:2;
then c6 in ].c1,c2.[ by E17, RCOMP_1:47;
hence not verum by E13, E19, RCOMP_1:48;
end;
end;
end;

theorem Th16: :: BORSUK_4:16
for b1, b2, b3, b4 being real number holds
( b1 < b2 & ].b1,b2.[ c= [.b3,b4.] implies [.b1,b2.] c= [.b3,b4.] )
proof
let c1, c2, c3, c4 be real number ;
assume E13: c1 < c2 ;
then E14: ].c1,c2.[ <> {} by RCOMP_1:15;
assume E15: ].c1,c2.[ c= [.c3,c4.] ;
then E16: ].c1,c2.[ meets [.c3,c4.] by E14, XBOOLE_1:69;
thus [.c1,c2.] c= [.c3,c4.]
proof
let c5 be set ; :: according to TARSKI:def 3
assume E17: c5 in [.c1,c2.] ;
per cases not ( not c5 = c1 & not c5 = c2 & not c5 in ].c1,c2.[ ) by E17, Th10;
suppose E18: c5 = c1 ;
now
per cases not ( c1 in [.c3,c4.] & not c1 in [.c3,c4.] ) ;
suppose E19: not c1 in [.c3,c4.] ;
now
per cases not ( not c1 < c3 & not c4 < c1 ) by E19, RCOMP_1:48;
suppose c1 < c3 ;
then consider c6 being real number such that
E20: ( c1 < c6 & c6 < c3 ) by XREAL_1:7;
c2 > c3 by E16, Th11;
then c6 < c2 by E20, XXREAL_0:2;
then c6 in ].c1,c2.[ by E20, RCOMP_1:47;
hence c5 in [.c3,c4.] by E15, E20, RCOMP_1:48;
end;
suppose c4 < c1 ;
hence c5 in [.c3,c4.] by E16, Th12;
end;
end;
end;
hence c5 in [.c3,c4.] ;
end;
suppose c1 in [.c3,c4.] ;
hence c5 in [.c3,c4.] by E18;
end;
end;
end;
hence c5 in [.c3,c4.] ;
end;
suppose E18: c5 = c2 ;
now
per cases not ( c2 in [.c3,c4.] & not c2 in [.c3,c4.] ) ;
suppose E19: not c2 in [.c3,c4.] ;
now
per cases not ( not c2 < c3 & not c4 < c2 ) by E19, RCOMP_1:48;
suppose c2 < c3 ;
then consider c6 being real number such that
E20: ( c2 < c6 & c6 < c3 ) by XREAL_1:7;
c2 > c3 by E16, Th11;
hence c5 in [.c3,c4.] by E20, XXREAL_0:2;
end;
suppose c4 < c2 ;
hence c5 in [.c3,c4.] by E13, E15, Th15;
end;
end;
end;
hence c5 in [.c3,c4.] ;
end;
suppose c2 in [.c3,c4.] ;
hence c5 in [.c3,c4.] by E18;
end;
end;
end;
hence c5 in [.c3,c4.] ;
end;
suppose c5 in ].c1,c2.[ ;
hence c5 in [.c3,c4.] by E15;
end;
end;
end;
end;

theorem Th17: :: BORSUK_4:17
for b1 being Subset of I[01]
for b2, b3 being real number holds
( b2 < b3 & b1 = ].b2,b3.[ implies [.b2,b3.] c= the carrier of I[01] )
proof
let c1 be Subset of I[01] ;
let c2, c3 be real number ;
assume E14: c2 < c3 ;
assume E15: c1 = ].c2,c3.[ ;
then E16: 0 <= c2 by E14, Th15, BORSUK_1:83;
c3 <= 1 by E14, E15, Th15, BORSUK_1:83;
hence [.c2,c3.] c= the carrier of I[01] by E16, BORSUK_1:83, TREAL_1:1;
end;

theorem Th18: :: BORSUK_4:18
for b1 being Subset of I[01]
for b2, b3 being real number holds
( b2 < b3 & b1 = ].b2,b3.] implies [.b2,b3.] c= the carrier of I[01] )
proof
let c1 be Subset of I[01] ;
let c2, c3 be real number ;
assume E15: c2 < c3 ;
E16: ].c2,c3.[ c= ].c2,c3.] by RCOMP_2:17;
assume c1 = ].c2,c3.] ;
then E17: ].c2,c3.[ c= [.0,1.] by E16, BORSUK_1:83, XBOOLE_1:1;
then E18: 0 <= c2 by E15, Th15;
c3 <= 1 by E15, E17, Th15;
hence [.c2,c3.] c= the carrier of I[01] by E18, BORSUK_1:83, TREAL_1:1;
end;

theorem Th19: :: BORSUK_4:19
for b1 being Subset of I[01]
for b2, b3 being real number holds
( b2 < b3 & b1 = [.b2,b3.[ implies [.b2,b3.] c= the carrier of I[01] )
proof
let c1 be Subset of I[01] ;
let c2, c3 be real number ;
assume E16: c2 < c3 ;
E17: ].c2,c3.[ c= [.c2,c3.[ by RCOMP_2:17;
assume c1 = [.c2,c3.[ ;
then E18: ].c2,c3.[ c= [.0,1.] by E17, BORSUK_1:83, XBOOLE_1:1;
then E19: 0 <= c2 by E16, Th15;
c3 <= 1 by E16, E18, Th15;
hence [.c2,c3.] c= the carrier of I[01] by E19, BORSUK_1:83, TREAL_1:1;
end;

theorem Th20: :: BORSUK_4:20
for b1, b2 being real number holds
( b1 <> b2 implies Cl ].b1,b2.] = [.b1,b2.] )
proof
let c1, c2 be real number ;
assume E17: c1 <> c2 ;
E18: ].c1,c2.] c= [.c1,c2.] by RCOMP_2:17;
E19: Cl ].c1,c2.] c= [.c1,c2.] by E18, PSCOMP_1:32;
].c1,c2.[ c= ].c1,c2.] by RCOMP_2:17;
then Cl ].c1,c2.[ c= Cl ].c1,c2.] by PSCOMP_1:37;
then [.c1,c2.] c= Cl ].c1,c2.] by E17, TOPREAL6:82;
hence Cl ].c1,c2.] = [.c1,c2.] by E19, XBOOLE_0:def 10;
end;

theorem Th21: :: BORSUK_4:21
for b1, b2 being real number holds
( b1 <> b2 implies Cl [.b1,b2.[ = [.b1,b2.] )
proof
let c1, c2 be real number ;
assume E18: c1 <> c2 ;
E19: [.c1,c2.[ c= [.c1,c2.] by RCOMP_2:17;
E20: Cl [.c1,c2.[ c= [.c1,c2.] by E19, PSCOMP_1:32;
].c1,c2.[ c= [.c1,c2.[ by RCOMP_2:17;
then Cl ].c1,c2.[ c= Cl [.c1,c2.[ by PSCOMP_1:37;
then [.c1,c2.] c= Cl [.c1,c2