:: BORSUK_6 semantic presentation

scheme :: BORSUK_6:sch 1
s1{ F₁() -> non empty set , P₁[ set ], P₂[ set ], P₃[ set ], F₂( set ) -> set , F₃( set ) -> set , F₄( set ) -> set } :

ex b₁ being Function st
( dom b₁ = F₁() & ( for b₂ being Element of F₁() holds
( ( P₁[b₂] implies b₁ . b₂ = F₂(b₂) ) & ( P₂[b₂] implies b₁ . b₂ = F₃(b₂) ) & ( P₃[b₂] implies b₁ . b₂ = F₄(b₂) ) ) ) )

provided

E1: for b₁ being Element of F₁() holds
( not ( P₁[b₁] & P₂[b₁] ) & not ( P₁[b₁] & P₃[b₁] ) & not ( P₂[b₁] & P₃[b₁] ) ) and E2: for b₁ being Element of F₁() holds
not ( not P₁[b₁] & not P₂[b₁] & not P₃[b₁] )

E3: for b₁ being set holds
( b₁ in F₁() implies ( not ( P₁[b₁] & P₂[b₁] ) & not ( P₁[b₁] & P₃[b₁] ) & not ( P₂[b₁] & P₃[b₁] ) ) ) by E1;
E4: for b₁ being set holds
not ( b₁ in F₁() & not P₁[b₁] & not P₂[b₁] & not P₃[b₁] ) by E2;
ex b₁ being Function st
( dom b₁ = F₁() & ( for b₂ being set holds
( b₂ in F₁() implies ( ( P₁[b₂] implies b₁ . b₂ = F₂(b₂) ) & ( P₂[b₂] implies b₁ . b₂ = F₃(b₂) ) & ( P₃[b₂] implies b₁ . b₂ = F₄(b₂) ) ) ) ) ) from RECDEF_2:sch 1(E3, E4);
then consider c₁ being Function such that
E5: dom c₁ = F₁() and
E6: for b₁ being set holds
( b₁ in F₁() implies ( ( P₁[b₁] implies c₁ . b₁ = F₂(b₁) ) & ( P₂[b₁] implies c₁ . b₁ = F₃(b₁) ) & ( P₃[b₁] implies c₁ . b₁ = F₄(b₁) ) ) ) ;
take c₁ ;
thus dom c₁ = F₁() by E5;
let c₂ be Element of F₁();
thus ( ( P₁[c₂] implies c₁ . c₂ = F₂(c₂) ) & ( P₂[c₂] implies c₁ . c₂ = F₃(c₂) ) & ( P₃[c₂] implies c₁ . c₂ = F₄(c₂) ) ) by E6;

end;

registration

let c₁ be Nat;
cluster TOP-REAL a₁ -> constituted-FinSeqs ;
coherence

let c₂ be Element of (TOP-REAL c₁); :: according to MONOID_0:def 2
thus c₂ is FinSequence by EUCLID:27;

end;

end;

theorem E1: :: BORSUK_6:1

the carrier of [:I[01] ,I[01] :] = [:[.0,1.],[.0,1.]:] by BORSUK_1:83, BORSUK_1:def 5;

E2: for b₁, b₂, b₃, b₄ being complex number holds (((b₄ - b₃) / b₂) * b₁) + b₃ = ((1 - (b₁ / b₂)) * b₃) + ((b₁ / b₂) * b₄)
by XCMPLX_1:236;

theorem :: BORSUK_6:2

canceled;

theorem :: BORSUK_6:3

canceled;

theorem :: BORSUK_6:4

canceled;

theorem E3: :: BORSUK_6:5

for b₁, b₂, b₃ being real number holds
( ( b₁ <= b₃ & b₃ <= b₂ ) implies ( (b₃ - b₁) / (b₂ - b₁) in the carrier of (Closed-Interval-TSpace 0,1) ) )

let c₁, c₂, c₃ be real number ;
assume E4: ( c₁ <= c₃ & c₃ <= c₂ ) ;
then E5: c₃ - c₁ <= c₂ - c₁ by XREAL_1:11;
E6: c₁ <= c₂ by E4, XXREAL_0:2;
then E7: c₂ - c₁ >= 0 by XREAL_1:50;
E8: (c₃ - c₁) / (c₂ - c₁) <= 1

per cases not ( not c₂ - c₁ = 0 & not c₂ - c₁ > 0 ) by E6, XREAL_1:50;

suppose c₂ - c₁ = 0 ;

hence (c₃ - c₁) / (c₂ - c₁) <= 1 by XCMPLX_1:49;

end;

suppose c₂ - c₁ > 0 ;

hence (c₃ - c₁) / (c₂ - c₁) <= 1 by E5, REAL_2:117;

end;

end;

end;

E9: c₃ - c₁ >= 0 by E4, XREAL_1:50;
(c₃ - c₁) / (c₂ - c₁) >= 0 by E7, E9, REAL_2:125;
then (c₃ - c₁) / (c₂ - c₁) in [.0,1.] by E8, RCOMP_1:48;
hence (c₃ - c₁) / (c₂ - c₁) in the carrier of (Closed-Interval-TSpace 0,1) by TOPMETR:25;

end;

theorem E4: :: BORSUK_6:6

for b₁ being Point of I[01] holds
( b₁ <= 1 / 2 implies 2 * b₁ is Point of I[01] )

let c₁ be Point of I[01] ;
assume c₁ <= 1 / 2 ;
then E5: 2 * c₁ <= 2 * (1 / 2) by XREAL_1:66;
0 <= c₁ by BORSUK_1:86;
then 2 * 0 <= 2 * c₁ by XREAL_1:66;
hence 2 * c₁ is Point of I[01] by E5, BORSUK_1:86;

end;

theorem E5: :: BORSUK_6:7

for b₁ being Point of I[01] holds
( b₁ >= 1 / 2 implies (2 * b₁) - 1 is Point of I[01] )

let c₁ be Point of I[01] ;
assume c₁ >= 1 / 2 ;
then 2 * c₁ >= 2 * (1 / 2) by XREAL_1:66;
then E6: (2 * c₁) - 1 >= 1 - 1 by XREAL_1:11;
c₁ <= 1 by BORSUK_1:86;
then 2 * c₁ <= 2 * 1 by XREAL_1:66;
then (2 * c₁) - 1 <= 2 - 1 by XREAL_1:11;
hence (2 * c₁) - 1 is Point of I[01] by E6, BORSUK_1:86;

end;

theorem E6: :: BORSUK_6:8

for b₁, b₂ being Point of I[01] holds
b₁ * b₂ is Point of I[01]

let c₁, c₂ be Point of I[01] ;
E7: ( 0 <= c₁ & c₁ <= 1 & 0 <= c₂ & c₂ <= 1 ) by BORSUK_1:86;
then E8: 0 <= c₁ * c₂ by REAL_2:121;
c₁ * c₂ <= 1 by E7, REAL_2:140;
hence c₁ * c₂ is Point of I[01] by E8, BORSUK_1:86;

end;

theorem E7: :: BORSUK_6:9

for b₁ being Point of I[01] holds
(1 / 2) * b₁ is Point of I[01]

let c₁ be Point of I[01] ;
c₁ >= 0 by BORSUK_1:86;
then E8: (1 / 2) * c₁ >= (1 / 2) * 0 by XREAL_1:66;
c₁ <= 1 by BORSUK_1:86;
then (1 / 2) * c₁ <= (1 / 2) * 1 by XREAL_1:66;
then (1 / 2) * c₁ <= 1 by XXREAL_0:2;
hence (1 / 2) * c₁ is Point of I[01] by E8, BORSUK_1:86;

end;

theorem E8: :: BORSUK_6:10

for b₁ being Point of I[01] holds
( b₁ >= 1 / 2 implies b₁ - (1 / 4) is Point of I[01] )

let c₁ be Point of I[01] ;
assume c₁ >= 1 / 2 ;
then c₁ >= (1 / 4) + 0 by XXREAL_0:2;
then E9: c₁ - (1 / 4) >= 0 by XREAL_1:21;
c₁ <= 1 by BORSUK_1:86;
then c₁ <= 1 + (1 / 4) by XXREAL_0:2;
then c₁ - (1 / 4) <= 1 by XREAL_1:22;
hence c₁ - (1 / 4) is Point of I[01] by E9, BORSUK_1:86;

end;

theorem :: BORSUK_6:11

canceled;

theorem E9: :: BORSUK_6:12

id I[01] is Path of 0[01] , 1[01]

set c₁ = id I[01] ;
( (id I[01] ) . 0 = 0[01] & (id I[01] ) . 1 = 1[01] ) by BORSUK_1:def 17, BORSUK_1:def 18, TMAP_1:91;
hence id I[01] is Path of 0[01] , 1[01] by BORSUK_2:def 4;

end;

theorem E10: :: BORSUK_6:13

for b₁, b₂, b₃, b₄ being Point of I[01] holds
( ( b₁ <= b₂ & b₃ <= b₄ ) implies ( [:[.b₁,b₂.],[.b₃,b₄.]:] is non empty compact Subset of [:I[01] ,I[01] :] ) )

let c₁, c₂, c₃, c₄ be Point of I[01] ;
assume that
E11: c₁ <= c₂ and
E12: c₃ <= c₄ ;
E13: [.c₁,c₂.] is Subset of I[01] by BORSUK_4:43;
[.c₃,c₄.] is Subset of I[01] by BORSUK_4:43;
then E14: [:[.c₁,c₂.],[.c₃,c₄.]:] c= [:the carrier of I[01] ,the carrier of I[01] :] by E13, ZFMISC_1:119;
E15: c₁ in [.c₁,c₂.] by E11, RCOMP_1:48;
c₃ in [.c₃,c₄.] by E12, RCOMP_1:48;
then reconsider c₅ = [:[.c₁,c₂.],[.c₃,c₄.]:] as non empty Subset of [:I[01] ,I[01] :] by E14, E15, BORSUK_1:def 5, ZFMISC_1:106;
( [.c₁,c₂.] is compact Subset of I[01] & [.c₃,c₄.] is compact Subset of I[01] ) by E11, E12, BORSUK_4:49;
then c₅ is compact Subset of [:I[01] ,I[01] :] by BORSUK_3:27;
hence [:[.c₁,c₂.],[.c₃,c₄.]:] is non empty compact Subset of [:I[01] ,I[01] :] ;

end;

theorem E11: :: BORSUK_6:14

for b₁, b₂ being Subset of (TOP-REAL 2) holds
( ( b₁ = { b₃ where B is Point of (TOP-REAL 2) : b₃ `2 <= (2 * (b₃ `1 )) - 1 } & b₂ = { b₃ where B is Point of (TOP-REAL 2) : b₃ `2 <= b₃ `1 } ) implies ( (AffineMap 1,0,(1 / 2),(1 / 2)) .: b₁ = b₂ ) )

let c₁, c₂ be Subset of (TOP-REAL 2);
assume E12: ( c₁ = { b₁ where B is Point of (TOP-REAL 2) : b₁ `2 <= (2 * (b₁ `1 )) - 1 } & c₂ = { b₁ where B is Point of (TOP-REAL 2) : b₁ `2 <= b₁ `1 } ) ;
set c₃ = 1;
set c₄ = 0;
set c₅ = 1 / 2;
set c₆ = 1 / 2;
set c₇ = AffineMap 1,0,(1 / 2),(1 / 2);
(AffineMap 1,0,(1 / 2),(1 / 2)) .: c₁ = c₂

thus (AffineMap 1,0,(1 / 2),(1 / 2)) .: c₁ c= c₂ :: according to XBOOLE_0:def 10

let c₈ be set ; :: according to TARSKI:def 3
assume c₈ in (AffineMap 1,0,(1 / 2),(1 / 2)) .: c₁ ;
then consider c₉ being set such that
E13: ( c₉ in dom (AffineMap 1,0,(1 / 2),(1 / 2)) & c₉ in c₁ & c₈ = (AffineMap 1,0,(1 / 2),(1 / 2)) . c₉ ) by FUNCT_1:def 12;
consider c₁₀ being Point of (TOP-REAL 2) such that
E14: ( c₉ = c₁₀ & c₁₀ `2 <= (2 * (c₁₀ `1 )) - 1 ) by E12, E13;
set c₁₁ = (AffineMap 1,0,(1 / 2),(1 / 2)) . c₁₀;
E15: (AffineMap 1,0,(1 / 2),(1 / 2)) . c₁₀ = |[((1 * (c₁₀ `1 )) + 0),(((1 / 2) * (c₁₀ `2 )) + (1 / 2))]| by JGRAPH_2:def 2;
then E16: ((AffineMap 1,0,(1 / 2),(1 / 2)) . c₁₀) `1 = (1 * (c₁₀ `1 )) + 0 by EUCLID:56;
E17: ((AffineMap 1,0,(1 / 2),(1 / 2)) . c₁₀) `2 = ((1 / 2) * (c₁₀ `2 )) + (1 / 2) by E15, EUCLID:56;
(1 / 2) * (c₁₀ `2 ) <= (1 / 2) * ((2 * (c₁₀ `1 )) - 1) by E14, XREAL_1:66;
then ((1 / 2) * (c₁₀ `2 )) + (1 / 2) <= ((c₁₀ `1 ) - (1 / 2)) + (1 / 2) by XREAL_1:8;
hence c₈ in c₂ by E12, E13, E14, E16, E17;

end;

let c₈ be set ; :: according to TARSKI:def 3
assume c₈ in c₂ ;
then consider c₉ being Point of (TOP-REAL 2) such that
E13: ( c₈ = c₉ & c₉ `2 <= c₉ `1 ) by E12;
AffineMap 1,0,(1 / 2),(1 / 2) is onto by JORDAN1K:36;
then rng (AffineMap 1,0,(1 / 2),(1 / 2)) = the carrier of (TOP-REAL 2) by FUNCT_2:def 3;
then consider c₁₀ being set such that
E14: ( c₁₀ in dom (AffineMap 1,0,(1 / 2),(1 / 2)) & c₈ = (AffineMap 1,0,(1 / 2),(1 / 2)) . c₁₀ ) by E13, FUNCT_1:def 5;
reconsider c₁₁ = c₁₀ as Point of (TOP-REAL 2) by E14;
set c₁₂ = (AffineMap 1,0,(1 / 2),(1 / 2)) . c₁₁;
E15: (AffineMap 1,0,(1 / 2),(1 / 2)) . c₁₁ = |[((1 * (c₁₁ `1 )) + 0),(((1 / 2) * (c₁₁ `2 )) + (1 / 2))]| by JGRAPH_2:def 2;
then E16: ((AffineMap 1,0,(1 / 2),(1 / 2)) . c₁₁) `1 = c₁₁ `1 by EUCLID:56;
E17: ((AffineMap 1,0,(1 / 2),(1 / 2)) . c₁₁) `2 = ((1 / 2) * (c₁₁ `2 )) + (1 / 2) by E15, EUCLID:56;
2 * (((AffineMap 1,0,(1 / 2),(1 / 2)) . c₁₁) `2 ) <= 2 * (c₁₁ `1 ) by E13, E14, E16, XREAL_1:66;
then (2 * (((AffineMap 1,0,(1 / 2),(1 / 2)) . c₁₁) `2 )) - 1 <= (2 * (c₁₁ `1 )) - 1 by XREAL_1:11;
then c₁₁ in c₁ by E12, E17;
hence c₈ in (AffineMap 1,0,(1 / 2),(1 / 2)) .: c₁ by E14, FUNCT_1:def 12;

end;

hence (AffineMap 1,0,(1 / 2),(1 / 2)) .: c₁ = c₂ ;

end;

theorem E12: :: BORSUK_6:15

for b₁, b₂ being Subset of (TOP-REAL 2) holds
( ( b₁ = { b₃ where B is Point of (TOP-REAL 2) : b₃ `2 >= (2 * (b₃ `1 )) - 1 } & b₂ = { b₃ where B is Point of (TOP-REAL 2) : b₃ `2 >= b₃ `1 } ) implies ( (AffineMap 1,0,(1 / 2),(1 / 2)) .: b₁ = b₂ ) )

let c₁, c₂ be Subset of (TOP-REAL 2);
assume E13: ( c₁ = { b₁ where B is Point of (TOP-REAL 2) : b₁ `2 >= (2 * (b₁ `1 )) - 1 } & c₂ = { b₁ where B is Point of (TOP-REAL 2) : b₁ `2 >= b₁ `1 } ) ;
set c₃ = 1;
set c₄ = 0;
set c₅ = 1 / 2;
set c₆ = 1 / 2;
set c₇ = AffineMap 1,0,(1 / 2),(1 / 2);
(AffineMap 1,0,(1 / 2),(1 / 2)) .: c₁ = c₂

thus (AffineMap 1,0,(1 / 2),(1 / 2)) .: c₁ c= c₂ :: according to XBOOLE_0:def 10

let c₈ be set ; :: according to TARSKI:def 3
assume c₈ in (AffineMap 1,0,(1 / 2),(1 / 2)) .: c₁ ;
then consider c₉ being set such that
E14: ( c₉ in dom (AffineMap 1,0,(1 / 2),(1 / 2)) & c₉ in c₁ & c₈ = (AffineMap 1,0,(1 / 2),(1 / 2)) . c₉ ) by FUNCT_1:def 12;
consider c₁₀ being Point of (TOP-REAL 2) such that
E15: ( c₉ = c₁₀ & c₁₀ `2 >= (2 * (c₁₀ `1 )) - 1 ) by E13, E14;
set c₁₁ = (AffineMap 1,0,(1 / 2),(1 / 2)) . c₁₀;
E16: (AffineMap 1,0,(1 / 2),(1 / 2)) . c₁₀ = |[((1 * (c₁₀ `1 )) + 0),(((1 / 2) * (c₁₀ `2 )) + (1 / 2))]| by JGRAPH_2:def 2;
then E17: ((AffineMap 1,0,(1 / 2),(1 / 2)) . c₁₀) `1 = (1 * (c₁₀ `1 )) + 0 by EUCLID:56;
E18: ((AffineMap 1,0,(1 / 2),(1 / 2)) . c₁₀) `2 = ((1 / 2) * (c₁₀ `2 )) + (1 / 2) by E16, EUCLID:56;
(1 / 2) * (c₁₀ `2 ) >= (1 / 2) * ((2 * (c₁₀ `1 )) - 1) by E15, XREAL_1:66;
then ((AffineMap 1,0,(1 / 2),(1 / 2)) . c₁₀) `2 >= ((c₁₀ `1 ) - (1 / 2)) + (1 / 2) by E18, XREAL_1:8;
hence c₈ in c₂ by E13, E14, E15, E17;

end;

let c₈ be set ; :: according to TARSKI:def 3
assume c₈ in c₂ ;
then consider c₉ being Point of (TOP-REAL 2) such that
E14: ( c₈ = c₉ & c₉ `2 >= c₉ `1 ) by E13;
AffineMap 1,0,(1 / 2),(1 / 2) is onto by JORDAN1K:36;
then rng (AffineMap 1,0,(1 / 2),(1 / 2)) = the carrier of (TOP-REAL 2) by FUNCT_2:def 3;
then consider c₁₀ being set such that
E15: ( c₁₀ in dom (AffineMap 1,0,(1 / 2),(1 / 2)) & c₈ = (AffineMap 1,0,(1 / 2),(1 / 2)) . c₁₀ ) by E14, FUNCT_1:def 5;
reconsider c₁₁ = c₁₀ as Point of (TOP-REAL 2) by E15;
set c₁₂ = (AffineMap 1,0,(1 / 2),(1 / 2)) . c₁₁;
E16: (AffineMap 1,0,(1 / 2),(1 / 2)) . c₁₁ = |[((1 * (c₁₁ `1 )) + 0),(((1 / 2) * (c₁₁ `2 )) + (1 / 2))]| by JGRAPH_2:def 2;
then E17: ((AffineMap 1,0,(1 / 2),(1 / 2)) . c₁₁) `1 = c₁₁ `1 by EUCLID:56;
E18: ((AffineMap 1,0,(1 / 2),(1 / 2)) . c₁₁) `2 = ((1 / 2) * (c₁₁ `2 )) + (1 / 2) by E16, EUCLID:56;
2 * (((AffineMap 1,0,(1 / 2),(1 / 2)) . c₁₁) `2 ) >= 2 * (c₁₁ `1 ) by E14, E15, E17, XREAL_1:66;
then (2 * (((AffineMap 1,0,(1 / 2),(1 / 2)) . c₁₁) `2 )) - 1 >= (2 * (c₁₁ `1 )) - 1 by XREAL_1:11;
then c₁₁ in c₁ by E13, E18;
hence c₈ in (AffineMap 1,0,(1 / 2),(1 / 2)) .: c₁ by E15, FUNCT_1:def 12;

end;

hence (AffineMap 1,0,(1 / 2),(1 / 2)) .: c₁ = c₂ ;

end;

theorem E13: :: BORSUK_6:16

for b₁, b₂ being Subset of (TOP-REAL 2) holds
( ( b₁ = { b₃ where B is Point of (TOP-REAL 2) : b₃ `2 >= 1 - (2 * (b₃ `1 )) } & b₂ = { b₃ where B is Point of (TOP-REAL 2) : b₃ `2 >= - (b₃ `1 ) } ) implies ( (AffineMap 1,0,(1 / 2),(- (1 / 2))) .: b₁ = b₂ ) )

let c₁, c₂ be Subset of (TOP-REAL 2);
assume E14: ( c₁ = { b₁ where B is Point of (TOP-REAL 2) : b₁ `2 >= 1 - (2 * (b₁ `1 )) } & c₂ = { b₁ where B is Point of (TOP-REAL 2) : b₁ `2 >= - (b₁ `1 ) } ) ;
set c₃ = 1;
set c₄ = 0;
set c₅ = 1 / 2;
set c₆ = - (1 / 2);
set c₇ = AffineMap 1,0,(1 / 2),(- (1 / 2));
(AffineMap 1,0,(1 / 2),(- (1 / 2))) .: c₁ = c₂

thus (AffineMap 1,0,(1 / 2),(- (1 / 2))) .: c₁ c= c₂ :: according to XBOOLE_0:def 10

let c₈ be set ; :: according to TARSKI:def 3
assume c₈ in (AffineMap 1,0,(1 / 2),(- (1 / 2))) .: c₁ ;
then consider c₉ being set such that
E15: ( c₉ in dom (AffineMap 1,0,(1 / 2),(- (1 / 2))) & c₉ in c₁ & c₈ = (AffineMap 1,0,(1 / 2),(- (1 / 2))) . c₉ ) by FUNCT_1:def 12;
consider c₁₀ being Point of (TOP-REAL 2) such that
E16: ( c₉ = c₁₀ & c₁₀ `2 >= 1 - (2 * (c₁₀ `1 )) ) by E14, E15;
set c₁₁ = (AffineMap 1,0,(1 / 2),(- (1 / 2))) . c₁₀;
E17: (AffineMap 1,0,(1 / 2),(- (1 / 2))) . c₁₀ = |[((1 * (c₁₀ `1 )) + 0),(((1 / 2) * (c₁₀ `2 )) + (- (1 / 2)))]| by JGRAPH_2:def 2;
then E18: ((AffineMap 1,0,(1 / 2),(- (1 / 2))) . c₁₀) `1 = (1 * (c₁₀ `1 )) + 0 by EUCLID:56;
(1 / 2) * (c₁₀ `2 ) >= (1 / 2) * (1 - (2 * (c₁₀ `1 ))) by E16, XREAL_1:66;
then ((1 / 2) * (c₁₀ `2 )) + (- (1 / 2)) >= ((1 / 2) - (c₁₀ `1 )) + (- (1 / 2)) by XREAL_1:8;
then ((AffineMap 1,0,(1 / 2),(- (1 / 2))) . c₁₀) `2 >= - (((AffineMap 1,0,(1 / 2),(- (1 / 2))) . c₁₀) `1 ) by E17, E18, EUCLID:56;
hence c₈ in c₂ by E14, E15, E16;

end;

let c₈ be set ; :: according to TARSKI:def 3
assume c₈ in c₂ ;
then consider c₉ being Point of (TOP-REAL 2) such that
E15: ( c₈ = c₉ & c₉ `2 >= - (c₉ `1 ) ) by E14;
AffineMap 1,0,(1 / 2),(- (1 / 2)) is onto by JORDAN1K:36;
then rng (AffineMap 1,0,(1 / 2),(- (1 / 2))) = the carrier of (TOP-REAL 2) by FUNCT_2:def 3;
then consider c₁₀ being set such that
E16: ( c₁₀ in dom (AffineMap 1,0,(1 / 2),(- (1 / 2))) & c₈ = (AffineMap 1,0,(1 / 2),(- (1 / 2))) . c₁₀ ) by E15, FUNCT_1:def 5;
reconsider c₁₁ = c₁₀ as Point of (TOP-REAL 2) by E16;
set c₁₂ = (AffineMap 1,0,(1 / 2),(- (1 / 2))) . c₁₁;
E17: (AffineMap 1,0,(1 / 2),(- (1 / 2))) . c₁₁ = |[((1 * (c₁₁ `1 )) + 0),(((1 / 2) * (c₁₁ `2 )) + (- (1 / 2)))]| by JGRAPH_2:def 2;
then E18: ((AffineMap 1,0,(1 / 2),(- (1 / 2))) . c₁₁) `1 = c₁₁ `1 by EUCLID:56;
E19: ((AffineMap 1,0,(1 / 2),(- (1 / 2))) . c₁₁) `2 = ((1 / 2) * (c₁₁ `2 )) + (- (1 / 2)) by E17, EUCLID:56;
2 * (((AffineMap 1,0,(1 / 2),(- (1 / 2))) . c₁₁) `2 ) >= 2 * (- (c₁₁ `1 )) by E15, E16, E18, XREAL_1:66;
then (2 * (((AffineMap 1,0,(1 / 2),(- (1 / 2))) . c₁₁) `2 )) + 1 >= (2 * (- (c₁₁ `1 ))) + 1 by XREAL_1:8;
then c₁₁ `2 >= 1 - (2 * (c₁₁ `1 )) by E19;
then c₁₁ in c₁ by E14;
hence c₈ in (AffineMap 1,0,(1 / 2),(- (1 / 2))) .: c₁ by E16, FUNCT_1:def 12;

end;

hence (AffineMap 1,0,(1 / 2),(- (1 / 2))) .: c₁ = c₂ ;

end;

theorem E14: :: BORSUK_6:17

for b₁, b₂ being Subset of (TOP-REAL 2) holds
( ( b₁ = { b₃ where B is Point of (TOP-REAL 2) : b₃ `2 <= 1 - (2 * (b₃ `1 )) } & b₂ = { b₃ where B is Point of (TOP-REAL 2) : b₃ `2 <= - (b₃ `1 ) } ) implies ( (AffineMap 1,0,(1 / 2),(- (1 / 2))) .: b₁ = b₂ ) )

let c₁, c₂ be Subset of (TOP-REAL 2);
assume E15: ( c₁ = { b₁ where B is Point of (TOP-REAL 2) : b₁ `2 <= 1 - (2 * (b₁ `1 )) } & c₂ = { b₁ where B is Point of (TOP-REAL 2) : b₁ `2 <= - (b₁ `1 ) } ) ;
set c₃ = 1;
set c₄ = 0;
set c₅ = 1 / 2;
set c₆ = - (1 / 2);
set c₇ = AffineMap 1,0,(1 / 2),(- (1 / 2));
(AffineMap 1,0,(1 / 2),(- (1 / 2))) .: c₁ = c₂

thus (AffineMap 1,0,(1 / 2),(- (1 / 2))) .: c₁ c= c₂ :: according to XBOOLE_0:def 10

let c₈ be set ; :: according to TARSKI:def 3
assume c₈ in (AffineMap 1,0,(1 / 2),(- (1 / 2))) .: c₁ ;
then consider c₉ being set such that
E16: ( c₉ in dom (AffineMap 1,0,(1 / 2),(- (1 / 2))) & c₉ in c₁ & c₈ = (AffineMap 1,0,(1 / 2),(- (1 / 2))) . c₉ ) by FUNCT_1:def 12;
consider c₁₀ being Point of (TOP-REAL 2) such that
E17: ( c₉ = c₁₀ & c₁₀ `2 <= 1 - (2 * (c₁₀ `1 )) ) by E15, E16;
set c₁₁ = (AffineMap 1,0,(1 / 2),(- (1 / 2))) . c₁₀;
E18: (AffineMap 1,0,(1 / 2),(- (1 / 2))) . c₁₀ = |[((1 * (c₁₀ `1 )) + 0),(((1 / 2) * (c₁₀ `2 )) + (- (1 / 2)))]| by JGRAPH_2:def 2;
then E19: ((AffineMap 1,0,(1 / 2),(- (1 / 2))) . c₁₀) `1 = (1 * (c₁₀ `1 )) + 0 by EUCLID:56;
(1 / 2) * (c₁₀ `2 ) <= (1 / 2) * (1 - (2 * (c₁₀ `1 ))) by E17, XREAL_1:66;
then ((1 / 2) * (c₁₀ `2 )) + (- (1 / 2)) <= ((1 / 2) - (c₁₀ `1 )) + (- (1 / 2)) by XREAL_1:8;
then ((AffineMap 1,0,(1 / 2),(- (1 / 2))) . c₁₀) `2 <= - (((AffineMap 1,0,(1 / 2),(- (1 / 2))) . c₁₀) `1 ) by E18, E19, EUCLID:56;
hence c₈ in c₂ by E15, E16, E17;

end;

let c₈ be set ; :: according to TARSKI:def 3
assume c₈ in c₂ ;
then consider c₉ being Point of (TOP-REAL 2) such that
E16: ( c₈ = c₉ & c₉ `2 <= - (c₉ `1 ) ) by E15;
AffineMap 1,0,(1 / 2),(- (1 / 2)) is onto by JORDAN1K:36;
then rng (AffineMap 1,0,(1 / 2),(- (1 / 2))) = the carrier of (TOP-REAL 2) by FUNCT_2:def 3;
then consider c₁₀ being set such that
E17: ( c₁₀ in dom (AffineMap 1,0,(1 / 2),(- (1 / 2))) & c₈ = (AffineMap 1,0,(1 / 2),(- (1 / 2))) . c₁₀ ) by E16, FUNCT_1:def 5;
reconsider c₁₁ = c₁₀ as Point of (TOP-REAL 2) by E17;
set c₁₂ = (AffineMap 1,0,(1 / 2),(- (1 / 2))) . c₁₁;
E18: (AffineMap 1,0,(1 / 2),(- (1 / 2))) . c₁₁ = |[((1 * (c₁₁ `1 )) + 0),(((1 / 2) * (c₁₁ `2 )) + (- (1 / 2)))]| by JGRAPH_2:def 2;
then E19: ((AffineMap 1,0,(1 / 2),(- (1 / 2))) . c₁₁) `1 = c₁₁ `1 by EUCLID:56;
E20: ((AffineMap 1,0,(1 / 2),(- (1 / 2))) . c₁₁) `2 = ((1 / 2) * (c₁₁ `2 )) + (- (1 / 2)) by E18, EUCLID:56;
2 * (((AffineMap 1,0,(1 / 2),(- (1 / 2))) . c₁₁) `2 ) <= 2 * (- (c₁₁ `1 )) by E16, E17, E19, XREAL_1:66;
then (2 * (((AffineMap 1,0,(1 / 2),(- (1 / 2))) . c₁₁) `2 )) + 1 <= (2 * (- (c₁₁ `1 ))) + 1 by XREAL_1:8;
then c₁₁ `2 <= 1 - (2 * (c₁₁ `1 )) by E20;
then c₁₁ in c₁ by E15;
hence c₈ in (AffineMap 1,0,(1 / 2),(- (1 / 2))) .: c₁ by E17, FUNCT_1:def 12;

end;

hence (AffineMap 1,0,(1 / 2),(- (1 / 2))) .: c₁ = c₂ ;

end;

definition

let c₁ be 1-sorted ;
attr a₁ is real-membered means :E15: :: BORSUK_6:def 1
the carrier of a₁ is real-membered;

end;

:: deftheorem E15 defines real-membered BORSUK_6:def 1 :

theorem E16: :: BORSUK_6:18

for b₁ being non empty 1-sorted holds
( b₁ is real-membered iff for b₂ being Element of b₁ holds b₂ is real )

let c₁ be non empty 1-sorted ;

hereby

assume c₁ is real-membered ;
then E17: the carrier of c₁ is real-membered by E15;
let c₂ be Element of c₁;
thus c₂ is real by E17, MEMBERED:def 2;

end;

assume for b₁ being Element of c₁ holds b₁ is real ;
then for b₁ being set holds
( b₁ in the carrier of c₁ implies b₁ is real ) ;
then the carrier of c₁ is real-membered by MEMBERED:def 2;
hence c₁ is real-membered by E15;

end;

registration

cluster I[01] -> real-membered ;
coherence

for b₁ being Element of I[01] holds b₁ is real ;
hence I[01] is real-membered by E16;

end;

end;

registration

cluster non empty real-membered 1-sorted ;
existence

take I[01] ;
thus ( not I[01] is empty & I[01] is real-membered ) ;

end;

cluster non empty real-membered TopStruct ;
existence

take I[01] ;
thus ( not I[01] is empty & I[01] is real-membered ) ;

end;

end;