:: BORSUK_6 semantic presentation

scheme :: BORSUK_6:sch 1
s1{ F1() -> non empty set , P1[ set ], P2[ set ], P3[ set ], F2( set ) -> set , F3( set ) -> set , F4( set ) -> set } :
ex b1 being Function st
( dom b1 = F1() & ( for b2 being Element of F1() holds
( ( P1[b2] implies b1 . b2 = F2(b2) ) & ( P2[b2] implies b1 . b2 = F3(b2) ) & ( P3[b2] implies b1 . b2 = F4(b2) ) ) ) )
provided
E1: for b1 being Element of F1() holds
( not ( P1[b1] & P2[b1] ) & not ( P1[b1] & P3[b1] ) & not ( P2[b1] & P3[b1] ) ) and E2: for b1 being Element of F1() holds
not ( not P1[b1] & not P2[b1] & not P3[b1] )
proof
E3: for b1 being set holds
( b1 in F1() implies ( not ( P1[b1] & P2[b1] ) & not ( P1[b1] & P3[b1] ) & not ( P2[b1] & P3[b1] ) ) ) by E1;
E4: for b1 being set holds
not ( b1 in F1() & not P1[b1] & not P2[b1] & not P3[b1] ) by E2;
ex b1 being Function st
( dom b1 = F1() & ( for b2 being set holds
( b2 in F1() implies ( ( P1[b2] implies b1 . b2 = F2(b2) ) & ( P2[b2] implies b1 . b2 = F3(b2) ) & ( P3[b2] implies b1 . b2 = F4(b2) ) ) ) ) ) from RECDEF_2:sch 1(E3, E4);
 then consider c1 being Function such that
E5: dom c1 = F1() and
E6: for b1 being set holds
( b1 in F1() implies ( ( P1[b1] implies c1 . b1 = F2(b1) ) & ( P2[b1] implies c1 . b1 = F3(b1) ) & ( P3[b1] implies c1 . b1 = F4(b1) ) ) ) ;
take c1 ;
thus dom c1 = F1() by E5;
let c2 be Element of F1();
thus ( ( P1[c2] implies c1 . c2 = F2(c2) ) & ( P2[c2] implies c1 . c2 = F3(c2) ) & ( P3[c2] implies c1 . c2 = F4(c2) ) ) by E6;
end;

registration
let c1 be Nat;
cluster TOP-REAL a1 -> constituted-FinSeqs ;
coherence
TOP-REAL c1 is constituted-FinSeqs
proof
let c2 be Element of (TOP-REAL c1); :: according to MONOID_0:def 2
thus c2 is FinSequence by EUCLID:27;
end;
end;

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

Lemma2: for b1, b2, b3, b4 being complex number holds (((b4 - b3) / b2) * b1) + b3 = ((1 - (b1 / b2)) * b3) + ((b1 / b2) * b4)
by XCMPLX_1:236;

theorem Th2: :: BORSUK_6:2
canceled;

theorem Th3: :: BORSUK_6:3
canceled;

theorem Th4: :: BORSUK_6:4
canceled;

theorem Th5: :: BORSUK_6:5
for b1, b2, b3 being real number holds
( b1 <= b3 & b3 <= b2 implies (b3 - b1) / (b2 - b1) in the carrier of (Closed-Interval-TSpace 0,1) )
proof
let c1, c2, c3 be real number ;
assume E4: ( c1 <= c3 & c3 <= c2 ) ;
then E5: c3 - c1 <= c2 - c1 by XREAL_1:11;
E6: c1 <= c2 by E4, XXREAL_0:2;
then E7: c2 - c1 >= 0 by XREAL_1:50;
E8: (c3 - c1) / (c2 - c1) <= 1
proof
per cases not ( not c2 - c1 = 0 & not c2 - c1 > 0 ) by E6, XREAL_1:50;
suppose c2 - c1 = 0 ;
hence (c3 - c1) / (c2 - c1) <= 1 by XCMPLX_1:49;
end;
suppose c2 - c1 > 0 ;
hence (c3 - c1) / (c2 - c1) <= 1 by E5, REAL_2:117;
end;
end;
end;
E9: c3 - c1 >= 0 by E4, XREAL_1:50;
(c3 - c1) / (c2 - c1) >= 0 by E7, E9, REAL_2:125;
then (c3 - c1) / (c2 - c1) in [.0,1.] by E8, RCOMP_1:48;
hence (c3 - c1) / (c2 - c1) in the carrier of (Closed-Interval-TSpace 0,1) by TOPMETR:25;
end;

theorem Th6: :: BORSUK_6:6
for b1 being Point of I[01] holds
( b1 <= 1 / 2 implies 2 * b1 is Point of I[01] )
proof
let c1 be Point of I[01] ;
assume c1 <= 1 / 2 ;
then E5: 2 * c1 <= 2 * (1 / 2) by XREAL_1:66;
0 <= c1 by BORSUK_1:86;
then 2 * 0 <= 2 * c1 by XREAL_1:66;
hence 2 * c1 is Point of I[01] by E5, BORSUK_1:86;
end;

theorem Th7: :: BORSUK_6:7
for b1 being Point of I[01] holds
( b1 >= 1 / 2 implies (2 * b1) - 1 is Point of I[01] )
proof
let c1 be Point of I[01] ;
assume c1 >= 1 / 2 ;
then 2 * c1 >= 2 * (1 / 2) by XREAL_1:66;
then E6: (2 * c1) - 1 >= 1 - 1 by XREAL_1:11;
c1 <= 1 by BORSUK_1:86;
then 2 * c1 <= 2 * 1 by XREAL_1:66;
then (2 * c1) - 1 <= 2 - 1 by XREAL_1:11;
hence (2 * c1) - 1 is Point of I[01] by E6, BORSUK_1:86;
end;

theorem Th8: :: BORSUK_6:8
for b1, b2 being Point of I[01] holds
b1 * b2 is Point of I[01]
proof
let c1, c2 be Point of I[01] ;
E7: ( 0 <= c1 & c1 <= 1 & 0 <= c2 & c2 <= 1 ) by BORSUK_1:86;
then E8: 0 <= c1 * c2 by REAL_2:121;
c1 * c2 <= 1 by E7, REAL_2:140;
hence c1 * c2 is Point of I[01] by E8, BORSUK_1:86;
end;

theorem Th9: :: BORSUK_6:9
for b1 being Point of I[01] holds
(1 / 2) * b1 is Point of I[01]
proof
let c1 be Point of I[01] ;
c1 >= 0 by BORSUK_1:86;
then E8: (1 / 2) * c1 >= (1 / 2) * 0 by XREAL_1:66;
c1 <= 1 by BORSUK_1:86;
then (1 / 2) * c1 <= (1 / 2) * 1 by XREAL_1:66;
then (1 / 2) * c1 <= 1 by XXREAL_0:2;
hence (1 / 2) * c1 is Point of I[01] by E8, BORSUK_1:86;
end;

theorem Th10: :: BORSUK_6:10
for b1 being Point of I[01] holds
( b1 >= 1 / 2 implies b1 - (1 / 4) is Point of I[01] )
proof
let c1 be Point of I[01] ;
assume c1 >= 1 / 2 ;
then c1 >= (1 / 4) + 0 by XXREAL_0:2;
then E9: c1 - (1 / 4) >= 0 by XREAL_1:21;
c1 <= 1 by BORSUK_1:86;
then c1 <= 1 + (1 / 4) by XXREAL_0:2;
then c1 - (1 / 4) <= 1 by XREAL_1:22;
hence c1 - (1 / 4) is Point of I[01] by E9, BORSUK_1:86;
end;

theorem Th11: :: BORSUK_6:11
canceled;

theorem Th12: :: BORSUK_6:12
id I[01] is Path of 0[01] , 1[01]
proof
set c1 = 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 Th13: :: BORSUK_6:13
for b1, b2, b3, b4 being Point of I[01] holds
( b1 <= b2 & b3 <= b4 implies [:[.b1,b2.],[.b3,b4.]:] is non empty compact Subset of [:I[01] ,I[01] :] )
proof
let c1, c2, c3, c4 be Point of I[01] ;
assume that
E11: c1 <= c2 and
E12: c3 <= c4 ;
E13: [.c1,c2.] is Subset of I[01] by BORSUK_4:43;
[.c3,c4.] is Subset of I[01] by BORSUK_4:43;
then E14: [:[.c1,c2.],[.c3,c4.]:] c= [:the carrier of I[01] ,the carrier of I[01] :] by E13, ZFMISC_1:119;
E15: c1 in [.c1,c2.] by E11, RCOMP_1:48;
c3 in [.c3,c4.] by E12, RCOMP_1:48;
then reconsider c5 = [:[.c1,c2.],[.c3,c4.]:] as non empty Subset of [:I[01] ,I[01] :] by E14, E15, BORSUK_1:def 5, ZFMISC_1:106;
( [.c1,c2.] is compact Subset of I[01] & [.c3,c4.] is compact Subset of I[01] ) by E11, E12, BORSUK_4:49;
then c5 is compact Subset of [:I[01] ,I[01] :] by BORSUK_3:27;
hence [:[.c1,c2.],[.c3,c4.]:] is non empty compact Subset of [:I[01] ,I[01] :] ;
end;

theorem Th14: :: BORSUK_6:14
for b1, b2 being Subset of (TOP-REAL 2) holds
( b1 = { b3 where B is Point of (TOP-REAL 2) : b3 `2 <= (2 * (b3 `1 )) - 1 } & b2 = { b3 where B is Point of (TOP-REAL 2) : b3 `2 <= b3 `1 } implies (AffineMap 1,0,(1 / 2),(1 / 2)) .: b1 = b2 )
proof
let c1, c2 be Subset of (TOP-REAL 2);
assume E12: ( c1 = { b1 where B is Point of (TOP-REAL 2) : b1 `2 <= (2 * (b1 `1 )) - 1 } & c2 = { b1 where B is Point of (TOP-REAL 2) : b1 `2 <= b1 `1 } ) ;
set c3 = 1;
set c4 = 0;
set c5 = 1 / 2;
set c6 = 1 / 2;
set c7 = AffineMap 1,0,(1 / 2),(1 / 2);
(AffineMap 1,0,(1 / 2),(1 / 2)) .: c1 = c2
proof
thus (AffineMap 1,0,(1 / 2),(1 / 2)) .: c1 c= c2 :: according to XBOOLE_0:def 10
proof
let c8 be set ; :: according to TARSKI:def 3
assume c8 in (AffineMap 1,0,(1 / 2),(1 / 2)) .: c1 ;
then consider c9 being set such that
E13: ( c9 in dom (AffineMap 1,0,(1 / 2),(1 / 2)) & c9 in c1 & c8 = (AffineMap 1,0,(1 / 2),(1 / 2)) . c9 ) by FUNCT_1:def 12;
consider c10 being Point of (TOP-REAL 2) such that
E14: ( c9 = c10 & c10 `2 <= (2 * (c10 `1 )) - 1 ) by E12, E13;
set c11 = (AffineMap 1,0,(1 / 2),(1 / 2)) . c10;
E15: (AffineMap 1,0,(1 / 2),(1 / 2)) . c10 = |[((1 * (c10 `1 )) + 0),(((1 / 2) * (c10 `2 )) + (1 / 2))]| by JGRAPH_2:def 2;
then E16: ((AffineMap 1,0,(1 / 2),(1 / 2)) . c10) `1 = (1 * (c10 `1 )) + 0 by EUCLID:56;
E17: ((AffineMap 1,0,(1 / 2),(1 / 2)) . c10) `2 = ((1 / 2) * (c10 `2 )) + (1 / 2) by E15, EUCLID:56;
(1 / 2) * (c10 `2 ) <= (1 / 2) * ((2 * (c10 `1 )) - 1) by E14, XREAL_1:66;
then ((1 / 2) * (c10 `2 )) + (1 / 2) <= ((c10 `1 ) - (1 / 2)) + (1 / 2) by XREAL_1:8;
hence c8 in c2 by E12, E13, E14, E16, E17;
end;
let c8 be set ; :: according to TARSKI:def 3
assume c8 in c2 ;
then consider c9 being Point of (TOP-REAL 2) such that
E13: ( c8 = c9 & c9 `2 <= c9 `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 c10 being set such that
E14: ( c10 in dom (AffineMap 1,0,(1 / 2),(1 / 2)) & c8 = (AffineMap 1,0,(1 / 2),(1 / 2)) . c10 ) by E13, FUNCT_1:def 5;
reconsider c11 = c10 as Point of (TOP-REAL 2) by E14;
set c12 = (AffineMap 1,0,(1 / 2),(1 / 2)) . c11;
E15: (AffineMap 1,0,(1 / 2),(1 / 2)) . c11 = |[((1 * (c11 `1 )) + 0),(((1 / 2) * (c11 `2 )) + (1 / 2))]| by JGRAPH_2:def 2;
then E16: ((AffineMap 1,0,(1 / 2),(1 / 2)) . c11) `1 = c11 `1 by EUCLID:56;
E17: ((AffineMap 1,0,(1 / 2),(1 / 2)) . c11) `2 = ((1 / 2) * (c11 `2 )) + (1 / 2) by E15, EUCLID:56;
2 * (((AffineMap 1,0,(1 / 2),(1 / 2)) . c11) `2 ) <= 2 * (c11 `1 ) by E13, E14, E16, XREAL_1:66;
then (2 * (((AffineMap 1,0,(1 / 2),(1 / 2)) . c11) `2 )) - 1 <= (2 * (c11 `1 )) - 1 by XREAL_1:11;
then c11 in c1 by E12, E17;
hence c8 in (AffineMap 1,0,(1 / 2),(1 / 2)) .: c1 by E14, FUNCT_1:def 12;
end;
hence (AffineMap 1,0,(1 / 2),(1 / 2)) .: c1 = c2 ;
end;

theorem Th15: :: BORSUK_6:15
for b1, b2 being Subset of (TOP-REAL 2) holds
( b1 = { b3 where B is Point of (TOP-REAL 2) : b3 `2 >= (2 * (b3 `1 )) - 1 } & b2 = { b3 where B is Point of (TOP-REAL 2) : b3 `2 >= b3 `1 } implies (AffineMap 1,0,(1 / 2),(1 / 2)) .: b1 = b2 )
proof
let c1, c2 be Subset of (TOP-REAL 2);
assume E13: ( c1 = { b1 where B is Point of (TOP-REAL 2) : b1 `2 >= (2 * (b1 `1 )) - 1 } & c2 = { b1 where B is Point of (TOP-REAL 2) : b1 `2 >= b1 `1 } ) ;
set c3 = 1;
set c4 = 0;
set c5 = 1 / 2;
set c6 = 1 / 2;
set c7 = AffineMap 1,0,(1 / 2),(1 / 2);
(AffineMap 1,0,(1 / 2),(1 / 2)) .: c1 = c2
proof
thus (AffineMap 1,0,(1 / 2),(1 / 2)) .: c1 c= c2 :: according to XBOOLE_0:def 10
proof
let c8 be set ; :: according to TARSKI:def 3
assume c8 in (AffineMap 1,0,(1 / 2),(1 / 2)) .: c1 ;
then consider c9 being set such that
E14: ( c9 in dom (AffineMap 1,0,(1 / 2),(1 / 2)) & c9 in c1 & c8 = (AffineMap 1,0,(1 / 2),(1 / 2)) . c9 ) by FUNCT_1:def 12;
consider c10 being Point of (TOP-REAL 2) such that
E15: ( c9 = c10 & c10 `2 >= (2 * (c10 `1 )) - 1 ) by E13, E14;
set c11 = (AffineMap 1,0,(1 / 2),(1 / 2)) . c10;
E16: (AffineMap 1,0,(1 / 2),(1 / 2)) . c10 = |[((1 * (c10 `1 )) + 0),(((1 / 2) * (c10 `2 )) + (1 / 2))]| by JGRAPH_2:def 2;
then E17: ((AffineMap 1,0,(1 / 2),(1 / 2)) . c10) `1 = (1 * (c10 `1 )) + 0 by EUCLID:56;
E18: ((AffineMap 1,0,(1 / 2),(1 / 2)) . c10) `2 = ((1 / 2) * (c10 `2 )) + (1 / 2) by E16, EUCLID:56;
(1 / 2) * (c10 `2 ) >= (1 / 2) * ((2 * (c10 `1 )) - 1) by E15, XREAL_1:66;
then ((AffineMap 1,0,(1 / 2),(1 / 2)) . c10) `2 >= ((c10 `1 ) - (1 / 2)) + (1 / 2) by E18, XREAL_1:8;
hence c8 in c2 by E13, E14, E15, E17;
end;
let c8 be set ; :: according to TARSKI:def 3
assume c8 in c2 ;
then consider c9 being Point of (TOP-REAL 2) such that
E14: ( c8 = c9 & c9 `2 >= c9 `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 c10 being set such that
E15: ( c10 in dom (AffineMap 1,0,(1 / 2),(1 / 2)) & c8 = (AffineMap 1,0,(1 / 2),(1 / 2)) . c10 ) by E14, FUNCT_1:def 5;
reconsider c11 = c10 as Point of (TOP-REAL 2) by E15;
set c12 = (AffineMap 1,0,(1 / 2),(1 / 2)) . c11;
E16: (AffineMap 1,0,(1 / 2),(1 / 2)) . c11 = |[((1 * (c11 `1 )) + 0),(((1 / 2) * (c11 `2 )) + (1 / 2))]| by JGRAPH_2:def 2;
then E17: ((AffineMap 1,0,(1 / 2),(1 / 2)) . c11) `1 = c11 `1 by EUCLID:56;
E18: ((AffineMap 1,0,(1 / 2),(1 / 2)) . c11) `2 = ((1 / 2) * (c11 `2 )) + (1 / 2) by E16, EUCLID:56;
2 * (((AffineMap 1,0,(1 / 2),(1 / 2)) . c11) `2 ) >= 2 * (c11 `1 ) by E14, E15, E17, XREAL_1:66;
then (2 * (((AffineMap 1,0,(1 / 2),(1 / 2)) . c11) `2 )) - 1 >= (2 * (c11 `1 )) - 1 by XREAL_1:11;
then c11 in c1 by E13, E18;
hence c8 in (AffineMap 1,0,(1 / 2),(1 / 2)) .: c1 by E15, FUNCT_1:def 12;
end;
hence (AffineMap 1,0,(1 / 2),(1 / 2)) .: c1 = c2 ;
end;

theorem Th16: :: BORSUK_6:16
for b1, b2 being Subset of (TOP-REAL 2) holds
( b1 = { b3 where B is Point of (TOP-REAL 2) : b3 `2 >= 1 - (2 * (b3 `1 )) } & b2 = { b3 where B is Point of (TOP-REAL 2) : b3 `2 >= - (b3 `1 ) } implies (AffineMap 1,0,(1 / 2),(- (1 / 2))) .: b1 = b2 )
proof
let c1, c2 be Subset of (TOP-REAL 2);
assume E14: ( c1 = { b1 where B is Point of (TOP-REAL 2) : b1 `2 >= 1 - (2 * (b1 `1 )) } & c2 = { b1 where B is Point of (TOP-REAL 2) : b1 `2 >= - (b1 `1 ) } ) ;
set c3 = 1;
set c4 = 0;
set c5 = 1 / 2;
set c6 = - (1 / 2);
set c7 = AffineMap 1,0,(1 / 2),(- (1 / 2));
(AffineMap 1,0,(1 / 2),(- (1 / 2))) .: c1 = c2
proof
thus (AffineMap 1,0,(1 / 2),(- (1 / 2))) .: c1 c= c2 :: according to XBOOLE_0:def 10
proof
let c8 be set ; :: according to TARSKI:def 3
assume c8 in (AffineMap 1,0,(1 / 2),(- (1 / 2))) .: c1 ;
then consider c9 being set such that
E15: ( c9 in dom (AffineMap 1,0,(1 / 2),(- (1 / 2))) & c9 in c1 & c8 = (AffineMap 1,0,(1 / 2),(- (1 / 2))) . c9 ) by FUNCT_1:def 12;
consider c10 being Point of (TOP-REAL 2) such that
E16: ( c9 = c10 & c10 `2 >= 1 - (2 * (c10 `1 )) ) by E14, E15;
set c11 = (AffineMap 1,0,(1 / 2),(- (1 / 2))) . c10;
E17: (AffineMap 1,0,(1 / 2),(- (1 / 2))) . c10 = |[((1 * (c10 `1 )) + 0),(((1 / 2) * (c10 `2 )) + (- (1 / 2)))]| by JGRAPH_2:def 2;
then E18: ((AffineMap 1,0,(1 / 2),(- (1 / 2))) . c10) `1 = (1 * (c10 `1 )) + 0 by EUCLID:56;
(1 / 2) * (c10 `2 ) >= (1 / 2) * (1 - (2 * (c10 `1 ))) by E16, XREAL_1:66;
then ((1 / 2) * (c10 `2 )) + (- (1 / 2)) >= ((1 / 2) - (c10 `1 )) + (- (1 / 2)) by XREAL_1:8;
then ((AffineMap 1,0,(1 / 2),(- (1 / 2))) . c10) `2 >= - (((AffineMap 1,0,(1 / 2),(- (1 / 2))) . c10) `1 ) by E17, E18, EUCLID:56;
hence c8 in c2 by E14, E15, E16;
end;
let c8 be set ; :: according to TARSKI:def 3
assume c8 in c2 ;
then consider c9 being Point of (TOP-REAL 2) such that
E15: ( c8 = c9 & c9 `2 >= - (c9 `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 c10 being set such that
E16: ( c10 in dom (AffineMap 1,0,(1 / 2),(- (1 / 2))) & c8 = (AffineMap 1,0,(1 / 2),(- (1 / 2))) . c10 ) by E15, FUNCT_1:def 5;
reconsider c11 = c10 as Point of (TOP-REAL 2) by E16;
set c12 = (AffineMap 1,0,(1 / 2),(- (1 / 2))) . c11;
E17: (AffineMap 1,0,(1 / 2),(- (1 / 2))) . c11 = |[((1 * (c11 `1 )) + 0),(((1 / 2) * (c11 `2 )) + (- (1 / 2)))]| by JGRAPH_2:def 2;
then E18: ((AffineMap 1,0,(1 / 2),(- (1 / 2))) . c11) `1 = c11 `1 by EUCLID:56;
E19: ((AffineMap 1,0,(1 / 2),(- (1 / 2))) . c11) `2 = ((1 / 2) * (c11 `2 )) + (- (1 / 2)) by E17, EUCLID:56;
2 * (((AffineMap 1,0,(1 / 2),(- (1 / 2))) . c11) `2 ) >= 2 * (- (c11 `1 )) by E15, E16, E18, XREAL_1:66;
then (2 * (((AffineMap 1,0,(1 / 2),(- (1 / 2))) . c11) `2 )) + 1 >= (2 * (- (c11 `1 ))) + 1 by XREAL_1:8;
then c11 `2 >= 1 - (2 * (c11 `1 )) by E19;
then c11 in c1 by E14;
hence c8 in (AffineMap 1,0,(1 / 2),(- (1 / 2))) .: c1 by E16, FUNCT_1:def 12;
end;
hence (AffineMap 1,0,(1 / 2),(- (1 / 2))) .: c1 = c2 ;
end;

theorem Th17: :: BORSUK_6:17
for b1, b2 being Subset of (TOP-REAL 2) holds
( b1 = { b3 where B is Point of (TOP-REAL 2) : b3 `2 <= 1 - (2 * (b3 `1 )) } & b2 = { b3 where B is Point of (TOP-REAL 2) : b3 `2 <= - (b3 `1 ) } implies (AffineMap 1,0,(1 / 2),(- (1 / 2))) .: b1 = b2 )
proof
let c1, c2 be Subset of (TOP-REAL 2);
assume E15: ( c1 = { b1 where B is Point of (TOP-REAL 2) : b1 `2 <= 1 - (2 * (b1 `1 )) } & c2 = { b1 where B is Point of (TOP-REAL 2) : b1 `2 <= - (b1 `1 ) } ) ;
set c3 = 1;
set c4 = 0;
set c5 = 1 / 2;
set c6 = - (1 / 2);
set c7 = AffineMap 1,0,(1 / 2),(- (1 / 2));
(AffineMap 1,0,(1 / 2),(- (1 / 2))) .: c1 = c2
proof
thus (AffineMap 1,0,(1 / 2),(- (1 / 2))) .: c1 c= c2 :: according to XBOOLE_0:def 10
proof
let c8 be set ; :: according to TARSKI:def 3
assume c8 in (AffineMap 1,0,(1 / 2),(- (1 / 2))) .: c1 ;
then consider c9 being set such that
E16: ( c9 in dom (AffineMap 1,0,(1 / 2),(- (1 / 2))) & c9 in c1 & c8 = (AffineMap 1,0,(1 / 2),(- (1 / 2))) . c9 ) by FUNCT_1:def 12;
consider c10 being Point of (TOP-REAL 2) such that
E17: ( c9 = c10 & c10 `2 <= 1 - (2 * (c10 `1 )) ) by E15, E16;
set c11 = (AffineMap 1,0,(1 / 2),(- (1 / 2))) . c10;
E18: (AffineMap 1,0,(1 / 2),(- (1 / 2))) . c10 = |[((1 * (c10 `1 )) + 0),(((1 / 2) * (c10 `2 )) + (- (1 / 2)))]| by JGRAPH_2:def 2;
then E19: ((AffineMap 1,0,(1 / 2),(- (1 / 2))) . c10) `1 = (1 * (c10 `1 )) + 0 by EUCLID:56;
(1 / 2) * (c10 `2 ) <= (1 / 2) * (1 - (2 * (c10 `1 ))) by E17, XREAL_1:66;
then ((1 / 2) * (c10 `2 )) + (- (1 / 2)) <= ((1 / 2) - (c10 `1 )) + (- (1 / 2)) by XREAL_1:8;
then ((AffineMap 1,0,(1 / 2),(- (1 / 2))) . c10) `2 <= - (((AffineMap 1,0,(1 / 2),(- (1 / 2))) . c10) `1 ) by E18, E19, EUCLID:56;
hence c8 in c2 by E15, E16, E17;
end;
let c8 be set ; :: according to TARSKI:def 3
assume c8 in c2 ;
then consider c9 being Point of (TOP-REAL 2) such that
E16: ( c8 = c9 & c9 `2 <= - (c9 `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 c10 being set such that
E17: ( c10 in dom (AffineMap 1,0,(1 / 2),(- (1 / 2))) & c8 = (AffineMap 1,0,(1 / 2),(- (1 / 2))) . c10 ) by E16, FUNCT_1:def 5;
reconsider c11 = c10 as Point of (TOP-REAL 2) by E17;
set c12 = (AffineMap 1,0,(1 / 2),(- (1 / 2))) . c11;
E18: (AffineMap 1,0,(1 / 2),(- (1 / 2))) . c11 = |[((1 * (c11 `1 )) + 0),(((1 / 2) * (c11 `2 )) + (- (1 / 2)))]| by JGRAPH_2:def 2;
then E19: ((AffineMap 1,0,(1 / 2),(- (1 / 2))) . c11) `1 = c11 `1 by EUCLID:56;
E20: ((AffineMap 1,0,(1 / 2),(- (1 / 2))