set K1a = { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) } ;
set K0a = { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `2 <= p8 `1 & - (p8 `1) <= p8 `2 ) or ( p8 `2 >= p8 `1 & p8 `2 <= - (p8 `1) ) ) & p8 <> 0. (TOP-REAL 2) ) } ;
let B, K0, Kb be Subset of (TOP-REAL 2); :: thesis: ( B = {(0. (TOP-REAL 2))} & K0 = { p where p is Point of (TOP-REAL 2) : ( - 1 < p `1 & p `1 < 1 & - 1 < p `2 & p `2 < 1 ) } & Kb = { q where q is Point of (TOP-REAL 2) : ( ( - 1 = q `1 & - 1 <= q `2 & q `2 <= 1 ) or ( q `1 = 1 & - 1 <= q `2 & q `2 <= 1 ) or ( - 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) or ( 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) ) } implies ex f being Function of ((TOP-REAL 2) | (B `)),((TOP-REAL 2) | (B `)) st
( f is continuous & f is one-to-one & ( for t being Point of (TOP-REAL 2) st t in K0 & t <> 0. (TOP-REAL 2) holds
not f . t in K0 \/ Kb ) & ( for r being Point of (TOP-REAL 2) st not r in K0 \/ Kb holds
f . r in K0 ) & ( for s being Point of (TOP-REAL 2) st s in Kb holds
f . s = s ) ) )
assume A1: ( B = {(0. (TOP-REAL 2))} & K0 = { p where p is Point of (TOP-REAL 2) : ( - 1 < p `1 & p `1 < 1 & - 1 < p `2 & p `2 < 1 ) } & Kb = { q where q is Point of (TOP-REAL 2) : ( ( - 1 = q `1 & - 1 <= q `2 & q `2 <= 1 ) or ( q `1 = 1 & - 1 <= q `2 & q `2 <= 1 ) or ( - 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) or ( 1 = q `2 & - 1 <= q `1 & q `1 <= 1 ) ) } ) ; :: thesis: ex f being Function of ((TOP-REAL 2) | (B `)),((TOP-REAL 2) | (B `)) st
( f is continuous & f is one-to-one & ( for t being Point of (TOP-REAL 2) st t in K0 & t <> 0. (TOP-REAL 2) holds
not f . t in K0 \/ Kb ) & ( for r being Point of (TOP-REAL 2) st not r in K0 \/ Kb holds
f . r in K0 ) & ( for s being Point of (TOP-REAL 2) st s in Kb holds
f . s = s ) )
then reconsider D = B ` as non empty Subset of (TOP-REAL 2) by Th19;
A2: D ` = {(0. (TOP-REAL 2))} by A1;
A3: B ` = NonZero (TOP-REAL 2) by A1, SUBSET_1:def 5;
A4: for t being Point of (TOP-REAL 2) st t in K0 & t <> 0. (TOP-REAL 2) holds
not Out_In_Sq . t in K0 \/ Kb

proof

let t be Point of (TOP-REAL 2); :: thesis: ( t in K0 & t <> 0. (TOP-REAL 2) implies not Out_In_Sq . t in K0 \/ Kb )
assume that
A5: t in K0 and
A6: t <> 0. (TOP-REAL 2) ; :: thesis: not Out_In_Sq . t in K0 \/ Kb
A7: ex p3 being Point of (TOP-REAL 2) st
( p3 = t & - 1 < p3 `1 & p3 `1 < 1 & - 1 < p3 `2 & p3 `2 < 1 ) by A1, A5;

now

assume A8: Out_In_Sq . t in K0 \/ Kb ; :: thesis: contradiction

now

per cases ( Out_In_Sq . t in K0 or Out_In_Sq . t in Kb ) by A8, XBOOLE_0:def 3;

case Out_In_Sq . t in K0 ; :: thesis: contradiction

then consider p4 being Point of (TOP-REAL 2) such that
A9: p4 = Out_In_Sq . t and
A10: - 1 < p4 `1 and
A11: p4 `1 < 1 and
A12: - 1 < p4 `2 and
A13: p4 `2 < 1 by A1;

now

per cases ( ( t `2 <= t `1 & - (t `1) <= t `2 ) or ( t `2 >= t `1 & t `2 <= - (t `1) ) or ( not ( t `2 <= t `1 & - (t `1) <= t `2 ) & not ( t `2 >= t `1 & t `2 <= - (t `1) ) ) ) ;

case A14: ( ( t `2 <= t `1 & - (t `1) <= t `2 ) or ( t `2 >= t `1 & t `2 <= - (t `1) ) ) ; :: thesis: contradiction

then Out_In_Sq . t = |[(1 / (t `1)),(((t `2) / (t `1)) / (t `1))]| by A6, Def1;
then A15: p4 `1 = 1 / (t `1) by A9, EUCLID:56;

now

per cases ( t `1 >= 0 or t `1 < 0 ) ;

case A16: t `1 >= 0 ; :: thesis: contradiction

now

per cases ( t `1 > 0 or t `1 = 0 ) by A16;

case A17: t `1 > 0 ; :: thesis: contradiction

then (1 / (t `1)) * (t `1) < 1 * (t `1) by A11, A15, XREAL_1:70;
hence contradiction by A7, A17, XCMPLX_1:88; :: thesis: verum

end;

case A18: t `1 = 0 ; :: thesis: contradiction

then t `2 = 0 by A14;
hence contradiction by A6, A18, EUCLID:57, EUCLID:58; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

case A19: t `1 < 0 ; :: thesis: contradiction

then (- 1) * (t `1) > (1 / (t `1)) * (t `1) by A10, A15, XREAL_1:71;
then (- 1) * (t `1) > 1 by A19, XCMPLX_1:88;
then - (- (t `1)) <= - 1 by XREAL_1:26;
hence contradiction by A7; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

case A20: ( not ( t `2 <= t `1 & - (t `1) <= t `2 ) & not ( t `2 >= t `1 & t `2 <= - (t `1) ) ) ; :: thesis: contradiction

then Out_In_Sq . t = |[(((t `1) / (t `2)) / (t `2)),(1 / (t `2))]| by A6, Def1;
then A21: p4 `2 = 1 / (t `2) by A9, EUCLID:56;

now

per cases ( t `2 >= 0 or t `2 < 0 ) ;

case A22: t `2 >= 0 ; :: thesis: contradiction

now

per cases ( t `2 > 0 or t `2 = 0 ) by A22;

case A23: t `2 > 0 ; :: thesis: contradiction

then (1 / (t `2)) * (t `2) < 1 * (t `2) by A13, A21, XREAL_1:70;
hence contradiction by A7, A23, XCMPLX_1:88; :: thesis: verum

end;

case t `2 = 0 ; :: thesis: contradiction

hence contradiction by A20; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

case A24: t `2 < 0 ; :: thesis: contradiction

then (- 1) * (t `2) > (1 / (t `2)) * (t `2) by A12, A21, XREAL_1:71;
then (- 1) * (t `2) > 1 by A24, XCMPLX_1:88;
then - (- (t `2)) <= - 1 by XREAL_1:26;
hence contradiction by A7; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

case Out_In_Sq . t in Kb ; :: thesis: contradiction

then consider p4 being Point of (TOP-REAL 2) such that
A25: p4 = Out_In_Sq . t and
A26: ( ( - 1 = p4 `1 & - 1 <= p4 `2 & p4 `2 <= 1 ) or ( p4 `1 = 1 & - 1 <= p4 `2 & p4 `2 <= 1 ) or ( - 1 = p4 `2 & - 1 <= p4 `1 & p4 `1 <= 1 ) or ( 1 = p4 `2 & - 1 <= p4 `1 & p4 `1 <= 1 ) ) by A1;

now

per cases ( ( t `2 <= t `1 & - (t `1) <= t `2 ) or ( t `2 >= t `1 & t `2 <= - (t `1) ) or ( not ( t `2 <= t `1 & - (t `1) <= t `2 ) & not ( t `2 >= t `1 & t `2 <= - (t `1) ) ) ) ;

case A27: ( ( t `2 <= t `1 & - (t `1) <= t `2 ) or ( t `2 >= t `1 & t `2 <= - (t `1) ) ) ; :: thesis: contradiction

then A28: Out_In_Sq . t = |[(1 / (t `1)),(((t `2) / (t `1)) / (t `1))]| by A6, Def1;
then A29: p4 `1 = 1 / (t `1) by A25, EUCLID:56;

now

per cases ( ( - 1 = p4 `1 & - 1 <= p4 `2 & p4 `2 <= 1 ) or ( p4 `1 = 1 & - 1 <= p4 `2 & p4 `2 <= 1 ) or ( - 1 = p4 `2 & - 1 <= p4 `1 & p4 `1 <= 1 ) or ( 1 = p4 `2 & - 1 <= p4 `1 & p4 `1 <= 1 ) ) by A26;

case ( - 1 = p4 `1 & - 1 <= p4 `2 & p4 `2 <= 1 ) ; :: thesis: contradiction

then A30: (t `1) * ((t `1) ") = - (t `1) by A29;

now

per cases ( t `1 <> 0 or t `1 = 0 ) ;

case t `1 <> 0 ; :: thesis: contradiction

then - (t `1) = 1 by A30, XCMPLX_0:def 7;
hence contradiction by A7; :: thesis: verum

end;

case A31: t `1 = 0 ; :: thesis: contradiction

then t `2 = 0 by A27;
hence contradiction by A6, A31, EUCLID:57, EUCLID:58; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

case ( p4 `1 = 1 & - 1 <= p4 `2 & p4 `2 <= 1 ) ; :: thesis: contradiction

then A32: (t `1) * ((t `1) ") = t `1 by A29;

now

per cases ( t `1 <> 0 or t `1 = 0 ) ;

case t `1 <> 0 ; :: thesis: contradiction

hence contradiction by A7, A32, XCMPLX_0:def 7; :: thesis: verum

end;

case A33: t `1 = 0 ; :: thesis: contradiction

then t `2 = 0 by A27;
hence contradiction by A6, A33, EUCLID:57, EUCLID:58; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

case A34: ( - 1 = p4 `2 & - 1 <= p4 `1 & p4 `1 <= 1 ) ; :: thesis: contradiction

reconsider K01 = { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `2 <= p8 `1 & - (p8 `1) <= p8 `2 ) or ( p8 `2 >= p8 `1 & p8 `2 <= - (p8 `1) ) ) & p8 <> 0. (TOP-REAL 2) ) } as non empty Subset of ((TOP-REAL 2) | D) by A2, Th27;
A35: the carrier of (((TOP-REAL 2) | D) | K01) = [#] (((TOP-REAL 2) | D) | K01)
.= K01 by PRE_TOPC:def 10 ;
A36: dom (Out_In_Sq | K01) = (dom Out_In_Sq) /\ K01 by RELAT_1:90
.= D /\ K01 by A3, FUNCT_2:def 1
.= ([#] ((TOP-REAL 2) | D)) /\ K01 by PRE_TOPC:def 10
.= the carrier of ((TOP-REAL 2) | D) /\ K01
.= K01 by XBOOLE_1:28 ;
t in K01 by A6, A27;
then A37: (Out_In_Sq | K01) . t in rng (Out_In_Sq | K01) by A36, FUNCT_1:12;
rng (Out_In_Sq | K01) c= the carrier of (((TOP-REAL 2) | D) | K01) by Th25;
then A38: (Out_In_Sq | K01) . t in the carrier of (((TOP-REAL 2) | D) | K01) by A37;
t in K01 by A6, A27;
then Out_In_Sq . t in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `2 <= p8 `1 & - (p8 `1) <= p8 `2 ) or ( p8 `2 >= p8 `1 & p8 `2 <= - (p8 `1) ) ) & p8 <> 0. (TOP-REAL 2) ) } by A38, A35, FUNCT_1:72;
then A39: ex p5 being Point of (TOP-REAL 2) st
( p5 = p4 & ( ( p5 `2 <= p5 `1 & - (p5 `1) <= p5 `2 ) or ( p5 `2 >= p5 `1 & p5 `2 <= - (p5 `1) ) ) & p5 <> 0. (TOP-REAL 2) ) by A25;

now

per cases ( p4 `1 >= 1 or - 1 >= p4 `1 ) by A34, A39, XREAL_1:26;

case A40: p4 `1 >= 1 ; :: thesis: contradiction

then ((t `2) / (t `1)) / (t `1) = ((t `2) / (t `1)) * 1 by A29, A34, XXREAL_0:1
.= (t `2) * 1 by A29, A34, A40, XXREAL_0:1
.= t `2 ;
hence contradiction by A7, A25, A28, A34, EUCLID:56; :: thesis: verum

end;

case A41: - 1 >= p4 `1 ; :: thesis: contradiction

then ((t `2) / (t `1)) / (t `1) = ((t `2) / (t `1)) * (- 1) by A29, A34, XXREAL_0:1
.= - ((t `2) / (t `1))
.= - ((t `2) * (- 1)) by A29, A34, A41, XXREAL_0:1
.= t `2 ;
hence contradiction by A7, A25, A28, A34, EUCLID:56; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

case A42: ( 1 = p4 `2 & - 1 <= p4 `1 & p4 `1 <= 1 ) ; :: thesis: contradiction

reconsider K01 = { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `2 <= p8 `1 & - (p8 `1) <= p8 `2 ) or ( p8 `2 >= p8 `1 & p8 `2 <= - (p8 `1) ) ) & p8 <> 0. (TOP-REAL 2) ) } as non empty Subset of ((TOP-REAL 2) | D) by A2, Th27;
t in K01 by A6, A27;
then A43: Out_In_Sq . t = (Out_In_Sq | K01) . t by FUNCT_1:72;
dom (Out_In_Sq | K01) = (dom Out_In_Sq) /\ K01 by RELAT_1:90
.= D /\ K01 by A3, FUNCT_2:def 1
.= ([#] ((TOP-REAL 2) | D)) /\ K01 by PRE_TOPC:def 10
.= the carrier of ((TOP-REAL 2) | D) /\ K01
.= K01 by XBOOLE_1:28 ;
then t in dom (Out_In_Sq | K01) by A6, A27;
then A44: (Out_In_Sq | K01) . t in rng (Out_In_Sq | K01) by FUNCT_1:12;
rng (Out_In_Sq | K01) c= the carrier of (((TOP-REAL 2) | D) | K01) by Th25;
then A45: (Out_In_Sq | K01) . t in the carrier of (((TOP-REAL 2) | D) | K01) by A44;
the carrier of (((TOP-REAL 2) | D) | K01) = [#] (((TOP-REAL 2) | D) | K01)
.= K01 by PRE_TOPC:def 10 ;
then A46: ex p5 being Point of (TOP-REAL 2) st
( p5 = p4 & ( ( p5 `2 <= p5 `1 & - (p5 `1) <= p5 `2 ) or ( p5 `2 >= p5 `1 & p5 `2 <= - (p5 `1) ) ) & p5 <> 0. (TOP-REAL 2) ) by A25, A45, A43;

now

per cases ( p4 `1 >= 1 or - 1 >= p4 `1 ) by A42, A46, XREAL_1:27;

case A47: p4 `1 >= 1 ; :: thesis: contradiction

then ((t `2) / (t `1)) / (t `1) = ((t `2) / (t `1)) * 1 by A29, A42, XXREAL_0:1
.= (t `2) * 1 by A29, A42, A47, XXREAL_0:1
.= t `2 ;
hence contradiction by A7, A25, A28, A42, EUCLID:56; :: thesis: verum

end;

case A48: - 1 >= p4 `1 ; :: thesis: contradiction

then ((t `2) / (t `1)) / (t `1) = ((t `2) / (t `1)) * (- 1) by A29, A42, XXREAL_0:1
.= - ((t `2) / (t `1))
.= - ((t `2) * (- 1)) by A29, A42, A48, XXREAL_0:1
.= t `2 ;
hence contradiction by A7, A25, A28, A42, EUCLID:56; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

case A49: ( not ( t `2 <= t `1 & - (t `1) <= t `2 ) & not ( t `2 >= t `1 & t `2 <= - (t `1) ) ) ; :: thesis: contradiction

then A50: Out_In_Sq . t = |[(((t `1) / (t `2)) / (t `2)),(1 / (t `2))]| by A6, Def1;
then A51: p4 `2 = 1 / (t `2) by A25, EUCLID:56;

now

per cases ( ( - 1 = p4 `2 & - 1 <= p4 `1 & p4 `1 <= 1 ) or ( p4 `2 = 1 & - 1 <= p4 `1 & p4 `1 <= 1 ) or ( - 1 = p4 `1 & - 1 <= p4 `2 & p4 `2 <= 1 ) or ( 1 = p4 `1 & - 1 <= p4 `2 & p4 `2 <= 1 ) ) by A26;

case ( - 1 = p4 `2 & - 1 <= p4 `1 & p4 `1 <= 1 ) ; :: thesis: contradiction

then A52: (t `2) * ((t `2) ") = - (t `2) by A51;

now

per cases ( t `2 <> 0 or t `2 = 0 ) ;

case t `2 <> 0 ; :: thesis: contradiction

then - (t `2) = 1 by A52, XCMPLX_0:def 7;
hence contradiction by A7; :: thesis: verum

end;

case t `2 = 0 ; :: thesis: contradiction

hence contradiction by A49; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

case ( p4 `2 = 1 & - 1 <= p4 `1 & p4 `1 <= 1 ) ; :: thesis: contradiction

then A53: (t `2) * ((t `2) ") = t `2 by A51;

now

per cases ( t `2 <> 0 or t `2 = 0 ) ;

case t `2 <> 0 ; :: thesis: contradiction

hence contradiction by A7, A53, XCMPLX_0:def 7; :: thesis: verum

end;

case t `2 = 0 ; :: thesis: contradiction

hence contradiction by A49; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

case A54: ( - 1 = p4 `1 & - 1 <= p4 `2 & p4 `2 <= 1 ) ; :: thesis: contradiction

reconsider K11 = { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) } as non empty Subset of ((TOP-REAL 2) | D) by A2, Th28;
A55: dom (Out_In_Sq | K11) = (dom Out_In_Sq) /\ K11 by RELAT_1:90
.= D /\ K11 by A3, FUNCT_2:def 1
.= ([#] ((TOP-REAL 2) | D)) /\ K11 by PRE_TOPC:def 10
.= the carrier of ((TOP-REAL 2) | D) /\ K11
.= K11 by XBOOLE_1:28 ;
A56: ( ( t `1 <= t `2 & - (t `2) <= t `1 ) or ( t `1 >= t `2 & t `1 <= - (t `2) ) ) by A49, Th23;
then t in K11 by A6;
then A57: Out_In_Sq . t = (Out_In_Sq | K11) . t by FUNCT_1:72;
t in K11 by A6, A56;
then A58: (Out_In_Sq | K11) . t in rng (Out_In_Sq | K11) by A55, FUNCT_1:12;
rng (Out_In_Sq | K11) c= the carrier of (((TOP-REAL 2) | D) | K11) by Th26;
then A59: (Out_In_Sq | K11) . t in the carrier of (((TOP-REAL 2) | D) | K11) by A58;
the carrier of (((TOP-REAL 2) | D) | K11) = [#] (((TOP-REAL 2) | D) | K11)
.= K11 by PRE_TOPC:def 10 ;
then A60: ex p5 being Point of (TOP-REAL 2) st
( p5 = p4 & ( ( p5 `1 <= p5 `2 & - (p5 `2) <= p5 `1 ) or ( p5 `1 >= p5 `2 & p5 `1 <= - (p5 `2) ) ) & p5 <> 0. (TOP-REAL 2) ) by A25, A59, A57;

now

per cases ( p4 `2 >= 1 or - 1 >= p4 `2 ) by A54, A60, XREAL_1:26;

case A61: p4 `2 >= 1 ; :: thesis: contradiction

then ((t `1) / (t `2)) / (t `2) = ((t `1) / (t `2)) * 1 by A51, A54, XXREAL_0:1
.= (t `1) * 1 by A51, A54, A61, XXREAL_0:1
.= t `1 ;
hence contradiction by A7, A25, A50, A54, EUCLID:56; :: thesis: verum

end;

case A62: - 1 >= p4 `2 ; :: thesis: contradiction

then ((t `1) / (t `2)) / (t `2) = ((t `1) / (t `2)) * (- 1) by A51, A54, XXREAL_0:1
.= - ((t `1) / (t `2))
.= - ((t `1) * (- 1)) by A51, A54, A62, XXREAL_0:1
.= t `1 ;
hence contradiction by A7, A25, A50, A54, EUCLID:56; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

case A63: ( 1 = p4 `1 & - 1 <= p4 `2 & p4 `2 <= 1 ) ; :: thesis: contradiction

reconsider K11 = { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) } as non empty Subset of ((TOP-REAL 2) | D) by A2, Th28;
A64: the carrier of (((TOP-REAL 2) | D) | K11) = [#] (((TOP-REAL 2) | D) | K11)
.= K11 by PRE_TOPC:def 10 ;
A65: dom (Out_In_Sq | K11) = (dom Out_In_Sq) /\ K11 by RELAT_1:90
.= D /\ K11 by A3, FUNCT_2:def 1
.= ([#] ((TOP-REAL 2) | D)) /\ K11 by PRE_TOPC:def 10
.= the carrier of ((TOP-REAL 2) | D) /\ K11
.= K11 by XBOOLE_1:28 ;
A66: ( ( t `1 <= t `2 & - (t `2) <= t `1 ) or ( t `1 >= t `2 & t `1 <= - (t `2) ) ) by A49, Th23;
then t in K11 by A6;
then A67: (Out_In_Sq | K11) . t in rng (Out_In_Sq | K11) by A65, FUNCT_1:12;
rng (Out_In_Sq | K11) c= the carrier of (((TOP-REAL 2) | D) | K11) by Th26;
then A68: (Out_In_Sq | K11) . t in the carrier of (((TOP-REAL 2) | D) | K11) by A67;
t in K11 by A6, A66;
then Out_In_Sq . t in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) } by A68, A64, FUNCT_1:72;
then A69: ex p5 being Point of (TOP-REAL 2) st
( p5 = p4 & ( ( p5 `1 <= p5 `2 & - (p5 `2) <= p5 `1 ) or ( p5 `1 >= p5 `2 & p5 `1 <= - (p5 `2) ) ) & p5 <> 0. (TOP-REAL 2) ) by A25;

now

per cases ( p4 `2 >= 1 or - 1 >= p4 `2 ) by A63, A69, XREAL_1:27;

case A70: p4 `2 >= 1 ; :: thesis: contradiction

then ((t `1) / (t `2)) / (t `2) = ((t `1) / (t `2)) * 1 by A51, A63, XXREAL_0:1
.= (t `1) * 1 by A51, A63, A70, XXREAL_0:1
.= t `1 ;
hence contradiction by A7, A25, A50, A63, EUCLID:56; :: thesis: verum

end;

case A71: - 1 >= p4 `2 ; :: thesis: contradiction

then ((t `1) / (t `2)) / (t `2) = ((t `1) / (t `2)) * (- 1) by A51, A63, XXREAL_0:1
.= - ((t `1) / (t `2))
.= - ((t `1) * (- 1)) by A51, A63, A71, XXREAL_0:1
.= t `1 ;
hence contradiction by A7, A25, A50, A63, EUCLID:56; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence not Out_In_Sq . t in K0 \/ Kb ; :: thesis: verum

end;

A72: for t being Point of (TOP-REAL 2) st not t in K0 \/ Kb holds
Out_In_Sq . t in K0

proof

let t be Point of (TOP-REAL 2); :: thesis: ( not t in K0 \/ Kb implies Out_In_Sq . t in K0 )
assume A73: not t in K0 \/ Kb ; :: thesis: Out_In_Sq . t in K0
then A74: not t in K0 by XBOOLE_0:def 3;
then A75: not t = 0. (TOP-REAL 2) by A1, Th11;
then not t in {(0. (TOP-REAL 2))} by TARSKI:def 1;
then t in NonZero (TOP-REAL 2) by XBOOLE_0:def 5;
then Out_In_Sq . t in NonZero (TOP-REAL 2) by FUNCT_2:7;
then reconsider p4 = Out_In_Sq . t as Point of (TOP-REAL 2) ;
A76: not t in Kb by A73, XBOOLE_0:def 3;

now

per cases ( ( t `2 <= t `1 & - (t `1) <= t `2 ) or ( t `2 >= t `1 & t `2 <= - (t `1) ) or ( not ( t `2 <= t `1 & - (t `1) <= t `2 ) & not ( t `2 >= t `1 & t `2 <= - (t `1) ) ) ) ;

case A77: ( ( t `2 <= t `1 & - (t `1) <= t `2 ) or ( t `2 >= t `1 & t `2 <= - (t `1) ) ) ; :: thesis: Out_In_Sq . t in K0

A78: now

per cases ( t `1 > 0 or t `1 <= 0 ) ;

case A79: t `1 > 0 ; :: thesis: ( - 1 < 1 / (t `1) & 1 / (t `1) < 1 & - 1 < ((t `2) / (t `1)) / (t `1) & ((t `2) / (t `1)) / (t `1) < 1 )

now

per cases ( t `2 > 0 or t `2 <= 0 ) ;

case A80: t `2 > 0 ; :: thesis: ( - 1 < 1 / (t `1) & 1 / (t `1) < 1 & - 1 < ((t `2) / (t `1)) / (t `1) & ((t `2) / (t `1)) / (t `1) < 1 )

( - 1 >= t `1 or t `1 >= 1 or - 1 >= t `2 or t `2 >= 1 ) by A1, A74;
then A81: t `1 >= 1 by A77, A79, A80, XXREAL_0:2;
not t `1 = 1 by A1, A76, A77;
then A82: t `1 > 1 by A81, XXREAL_0:1;
then t `1 < (t `1) ^2 by SQUARE_1:76;
then t `2 < (t `1) ^2 by A77, A79, XXREAL_0:2;
then (t `2) / (t `1) < ((t `1) ^2) / (t `1) by A79, XREAL_1:76;
then (t `2) / (t `1) < t `1 by A79, XCMPLX_1:90;
then A83: ((t `2) / (t `1)) / (t `1) < (t `1) / (t `1) by A79, XREAL_1:76;
0 < (t `2) / (t `1) by A79, A80, XREAL_1:141;
then A84: ((- 1) * (t `1)) / (t `1) < ((t `2) / (t `1)) / (t `1) by A79, XREAL_1:76;
(t `1) / (t `1) > 1 / (t `1) by A82, XREAL_1:76;
hence ( - 1 < 1 / (t `1) & 1 / (t `1) < 1 & - 1 < ((t `2) / (t `1)) / (t `1) & ((t `2) / (t `1)) / (t `1) < 1 ) by A79, A84, A83, XCMPLX_1:60, XCMPLX_1:90; :: thesis: verum

end;

case A85: t `2 <= 0 ; :: thesis: ( - 1 < 1 / (t `1) & 1 / (t `1) < 1 & - 1 < ((t `2) / (t `1)) / (t `1) & ((t `2) / (t `1)) / (t `1) < 1 )

A86: now

assume t `1 < 1 ; :: thesis: t `1 >= 1
then - 1 >= t `2 by A1, A74, A79, A85;
then - (t `1) <= - 1 by A77, A79, XXREAL_0:2;
hence t `1 >= 1 by XREAL_1:26; :: thesis: verum

end;

not t `1 = 1 by A1, A76, A77;
then A87: t `1 > 1 by A86, XXREAL_0:1;
then A88: t `1 < (t `1) ^2 by SQUARE_1:76;
- (- (t `1)) >= - (t `2) by A77, A79, XREAL_1:26;
then (t `1) ^2 > - (t `2) by A88, XXREAL_0:2;
then ((t `1) ^2) / (t `1) > (- (t `2)) / (t `1) by A79, XREAL_1:76;
then t `1 > - ((t `2) / (t `1)) by A79, XCMPLX_1:90;
then - (t `1) < - (- ((t `2) / (t `1))) by XREAL_1:26;
then A89: ((- 1) * (t `1)) / (t `1) < ((t `2) / (t `1)) / (t `1) by A79, XREAL_1:76;
(t `1) / (t `1) > 1 / (t `1) by A87, XREAL_1:76;
hence ( - 1 < 1 / (t `1) & 1 / (t `1) < 1 & - 1 < ((t `2) / (t `1)) / (t `1) & ((t `2) / (t `1)) / (t `1) < 1 ) by A79, A85, A89, XCMPLX_1:60, XCMPLX_1:90; :: thesis: verum

end;

end;

end;

hence ( - 1 < 1 / (t `1) & 1 / (t `1) < 1 & - 1 < ((t `2) / (t `1)) / (t `1) & ((t `2) / (t `1)) / (t `1) < 1 ) ; :: thesis: verum

end;

case A90: t `1 <= 0 ; :: thesis: ( - 1 < 1 / (t `1) & 1 / (t `1) < 1 & - 1 < ((t `2) / (t `1)) / (t `1) & ((t `2) / (t `1)) / (t `1) < 1 )

now

per cases ( t `1 = 0 or t `1 < 0 ) by A90;

case A91: t `1 = 0 ; :: thesis: contradiction

then t `2 = 0 by A77;
hence contradiction by A1, A74, A91; :: thesis: verum

end;

case A92: t `1 < 0 ; :: thesis: ( - 1 < 1 / (t `1) & 1 / (t `1) < 1 & - 1 < ((t `2) / (t `1)) / (t `1) & ((t `2) / (t `1)) / (t `1) < 1 )

now

per cases ( t `2 > 0 or t `2 <= 0 ) ;

case A93: t `2 > 0 ; :: thesis: ( - 1 < 1 / (t `1) & 1 / (t `1) < 1 & - 1 < ((t `2) / (t `1)) / (t `1) & ((t `2) / (t `1)) / (t `1) < 1 )

( - 1 >= t `1 or t `1 >= 1 or - 1 >= t `2 or t `2 >= 1 ) by A1, A74;
then ( t `1 <= - 1 or 1 <= - (t `1) ) by A77, A92, XXREAL_0:2;
then A94: ( t `1 <= - 1 or - 1 >= - (- (t `1)) ) by XREAL_1:26;
not t `1 = - 1 by A1, A76, A77;
then A95: t `1 < - 1 by A94, XXREAL_0:1;
then (t `1) / (t `1) > (- 1) / (t `1) by XREAL_1:77;
then A96: - ((t `1) / (t `1)) < - ((- 1) / (t `1)) by XREAL_1:26;
- (t `1) < (t `1) ^2 by A95, SQUARE_1:116;
then t `2 < (t `1) ^2 by A77, A92, XXREAL_0:2;
then (t `2) / (t `1) > ((t `1) ^2) / (t `1) by A92, XREAL_1:77;
then (t `2) / (t `1) > t `1 by A92, XCMPLX_1:90;
then A97: ((t `2) / (t `1)) / (t `1) < (t `1) / (t `1) by A92, XREAL_1:77;
0 > (t `2) / (t `1) by A92, A93, XREAL_1:144;
then ((- 1) * (t `1)) / (t `1) < ((t `2) / (t `1)) / (t `1) by A92, XREAL_1:77;
hence ( - 1 < 1 / (t `1) & 1 / (t `1) < 1 & - 1 < ((t `2) / (t `1)) / (t `1) & ((t `2) / (t `1)) / (t `1) < 1 ) by A92, A96, A97, XCMPLX_1:60; :: thesis: verum

end;

case A98: t `2 <= 0 ; :: thesis: ( - 1 < 1 / (t `1) & 1 / (t `1) < 1 & - 1 < ((t `2) / (t `1)) / (t `1) & ((t `2) / (t `1)) / (t `1) < 1 )

then ( - 1 >= t `1 or - 1 >= t `2 ) by A1, A74, A92;
then A99: t `1 <= - 1 by A77, A92, XXREAL_0:2;
not t `1 = - 1 by A1, A76, A77;
then A100: t `1 < - 1 by A99, XXREAL_0:1;
then A101: - (t `1) < (t `1) ^2 by SQUARE_1:116;
- (t `1) >= - (t `2) by A77, A92, XREAL_1:26;
then (t `1) ^2 > - (t `2) by A101, XXREAL_0:2;
then ((t `1) ^2) / (t `1) < (- (t `2)) / (t `1) by A92, XREAL_1:77;
then t `1 < - ((t `2) / (t `1)) by A92, XCMPLX_1:90;
then - (t `1) > - (- ((t `2) / (t `1))) by XREAL_1:26;
then A102: ((- 1) * (t `1)) / (t `1) < ((t `2) / (t `1)) / (t `1) by A92, XREAL_1:77;
(t `1) / (t `1) > (- 1) / (t `1) by A100, XREAL_1:77;
then 1 > (- 1) / (t `1) by A92, XCMPLX_1:60;
then - 1 < - ((- 1) / (t `1)) by XREAL_1:26;
hence ( - 1 < 1 / (t `1) & 1 / (t `1) < 1 & - 1 < ((t `2) / (t `1)) / (t `1) & ((t `2) / (t `1)) / (t `1) < 1 ) by A92, A98, A102, XCMPLX_1:90; :: thesis: verum

end;

end;

end;

hence ( - 1 < 1 / (t `1) & 1 / (t `1) < 1 & - 1 < ((t `2) / (t `1)) / (t `1) & ((t `2) / (t `1)) / (t `1) < 1 ) ; :: thesis: verum

end;

end;

end;

hence ( - 1 < 1 / (t `1) & 1 / (t `1) < 1 & - 1 < ((t `2) / (t `1)) / (t `1) & ((t `2) / (t `1)) / (t `1) < 1 ) ; :: thesis: verum

end;

end;

end;

Out_In_Sq . t = |[(1 / (t `1)),(((t `2) / (t `1)) / (t `1))]| by A75, A77, Def1;
then ( p4 `1 = 1 / (t `1) & p4 `2 = ((t `2) / (t `1)) / (t `1) ) by EUCLID:56;
hence Out_In_Sq . t in K0 by A1, A78; :: thesis: verum

end;

case A103: ( not ( t `2 <= t `1 & - (t `1) <= t `2 ) & not ( t `2 >= t `1 & t `2 <= - (t `1) ) ) ; :: thesis: Out_In_Sq . t in K0

then A104: ( ( t `1 <= t `2 & - (t `2) <= t `1 ) or ( t `1 >= t `2 & t `1 <= - (t `2) ) ) by Th23;

A105: now

per cases ( t `2 > 0 or t `2 <= 0 ) ;

case A106: t `2 > 0 ; :: thesis: ( - 1 < 1 / (t `2) & 1 / (t `2) < 1 & - 1 < ((t `1) / (t `2)) / (t `2) & ((t `1) / (t `2)) / (t `2) < 1 )

now

per cases ( t `1 > 0 or t `1 <= 0 ) ;

case A107: t `1 > 0 ; :: thesis: ( - 1 < 1 / (t `2) & 1 / (t `2) < 1 & - 1 < ((t `1) / (t `2)) / (t `2) & ((t `1) / (t `2)) / (t `2) < 1 )

A108: ( - 1 >= t `2 or t `2 >= 1 or - 1 >= t `1 or t `1 >= 1 ) by A1, A74;
not t `2 = 1 by A1, A76, A103, A107;
then A109: t `2 > 1 by A103, A106, A107, A108, XXREAL_0:1, XXREAL_0:2;
then t `2 < (t `2) ^2 by SQUARE_1:76;
then t `1 < (t `2) ^2 by A103, A106, XXREAL_0:2;
then (t `1) / (t `2) < ((t `2) ^2) / (t `2) by A106, XREAL_1:76;
then (t `1) / (t `2) < t `2 by A106, XCMPLX_1:90;
then A110: ((t `1) / (t `2)) / (t `2) < (t `2) / (t `2) by A106, XREAL_1:76;
0 < (t `1) / (t `2) by A106, A107, XREAL_1:141;
then A111: ((- 1) * (t `2)) / (t `2) < ((t `1) / (t `2)) / (t `2) by A106, XREAL_1:76;
(t `2) / (t `2) > 1 / (t `2) by A109, XREAL_1:76;
hence ( - 1 < 1 / (t `2) & 1 / (t `2) < 1 & - 1 < ((t `1) / (t `2)) / (t `2) & ((t `1) / (t `2)) / (t `2) < 1 ) by A106, A111, A110, XCMPLX_1:60, XCMPLX_1:90; :: thesis: verum

end;

case A112: t `1 <= 0 ; :: thesis: ( - 1 < 1 / (t `2) & 1 / (t `2) < 1 & - 1 < ((t `1) / (t `2)) / (t `2) & ((t `1) / (t `2)) / (t `2) < 1 )

A113: now

assume t `2 < 1 ; :: thesis: t `2 >= 1
then - 1 >= t `1 by A1, A74, A106, A112;
then - (t `2) <= - 1 by A104, A106, XXREAL_0:2;
hence t `2 >= 1 by XREAL_1:26; :: thesis: verum

end;

not t `2 = 1 by A1, A76, A104;
then A114: t `2 > 1 by A113, XXREAL_0:1;
then t `2 < (t `2) ^2 by SQUARE_1:76;
then (t `2) ^2 > - (t `1) by A103, A106, XXREAL_0:2;
then ((t `2) ^2) / (t `2) > (- (t `1)) / (t `2) by A106, XREAL_1:76;
then t `2 > - ((t `1) / (t `2)) by A106, XCMPLX_1:90;
then - (t `2) < - (- ((t `1) / (t `2))) by XREAL_1:26;
then A115: ((- 1) * (t `2)) / (t `2) < ((t `1) / (t `2)) / (t `2) by A106, XREAL_1:76;
(t `2) / (t `2) > 1 / (t `2) by A114, XREAL_1:76;
hence ( - 1 < 1 / (t `2) & 1 / (t `2) < 1 & - 1 < ((t `1) / (t `2)) / (t `2) & ((t `1) / (t `2)) / (t `2) < 1 ) by A106, A112, A115, XCMPLX_1:60, XCMPLX_1:90; :: thesis: verum

end;

end;

end;

hence ( - 1 < 1 / (t `2) & 1 / (t `2) < 1 & - 1 < ((t `1) / (t `2)) / (t `2) & ((t `1) / (t `2)) / (t `2) < 1 ) ; :: thesis: verum

end;

case A116: t `2 <= 0 ; :: thesis: ( - 1 < 1 / (t `2) & 1 / (t `2) < 1 & - 1 < ((t `1) / (t `2)) / (t `2) & ((t `1) / (t `2)) / (t `2) < 1 )

then A117: t `2 < 0 by A103;
A118: ( t `1 <= t `2 or t `1 <= - (t `2) ) by A103, Th23;

now

per cases ( t `1 > 0 or t `1 <= 0 ) ;

case A119: t `1 > 0 ; :: thesis: ( - 1 < 1 / (t `2) & 1 / (t `2) < 1 & - 1 < ((t `1) / (t `2)) / (t `2) & ((t `1) / (t `2)) / (t `2) < 1 )

( - 1 >= t `2 or t `2 >= 1 or - 1 >= t `1 or t `1 >= 1 ) by A1, A74;
then ( t `2 <= - 1 or 1 <= - (t `2) ) by A104, A116, XXREAL_0:2;
then A120: ( t `2 <= - 1 or - 1 >= - (- (t `2)) ) by XREAL_1:26;
not t `2 = - 1 by A1, A76, A104;
then A121: t `2 < - 1 by A120, XXREAL_0:1;
then (t `2) / (t `2) > (- 1) / (t `2) by XREAL_1:77;
then A122: - ((t `2) / (t `2)) < - ((- 1) / (t `2)) by XREAL_1:26;
- (t `2) < (t `2) ^2 by A121, SQUARE_1:116;
then t `1 < (t `2) ^2 by A116, A118, XXREAL_0:2;
then (t `1) / (t `2) > ((t `2) ^2) / (t `2) by A117, XREAL_1:77;
then (t `1) / (t `2) > t `2 by A117, XCMPLX_1:90;
then A123: ((t `1) / (t `2)) / (t `2) < (t `2) / (t `2) by A117, XREAL_1:77;
0 > (t `1) / (t `2) by A117, A119, XREAL_1:144;
then ((- 1) * (t `2)) / (t `2) < ((t `1) / (t `2)) / (t `2) by A117, XREAL_1:77;
hence ( - 1 < 1 / (t `2) & 1 / (t `2) < 1 & - 1 < ((t `1) / (t `2)) / (t `2) & ((t `1) / (t `2)) / (t `2) < 1 ) by A117, A122, A123, XCMPLX_1:60; :: thesis: verum

end;

case A124: t `1 <= 0 ; :: thesis: ( - 1 < 1 / (t `2) & 1 / (t `2) < 1 & - 1 < ((t `1) / (t `2)) / (t `2) & ((t `1) / (t `2)) / (t `2) < 1 )

A125: not t `2 = - 1 by A1, A76, A104;
( - 1 >= t `2 or - 1 >= t `1 ) by A1, A74, A116, A124;
then A126: t `2 < - 1 by A103, A116, A125, XXREAL_0:1, XXREAL_0:2;
then A127: - (t `2) < (t `2) ^2 by SQUARE_1:116;
- (t `2) >= - (t `1) by A103, A116, XREAL_1:26;
then (t `2) ^2 > - (t `1) by A127, XXREAL_0:2;
then ((t `2) ^2) / (t `2) < (- (t `1)) / (t `2) by A117, XREAL_1:77;
then t `2 < - ((t `1) / (t `2)) by A117, XCMPLX_1:90;
then - (t `2) > - (- ((t `1) / (t `2))) by XREAL_1:26;
then A128: ((- 1) * (t `2)) / (t `2) < ((t `1) / (t `2)) / (t `2) by A117, XREAL_1:77;
(t `2) / (t `2) > (- 1) / (t `2) by A126, XREAL_1:77;
then 1 > (- 1) / (t `2) by A117, XCMPLX_1:60;
then - 1 < - ((- 1) / (t `2)) by XREAL_1:26;
hence ( - 1 < 1 / (t `2) & 1 / (t `2) < 1 & - 1 < ((t `1) / (t `2)) / (t `2) & ((t `1) / (t `2)) / (t `2) < 1 ) by A103, A116, A124, A128, XCMPLX_1:90; :: thesis: verum

end;

end;

end;

hence ( - 1 < 1 / (t `2) & 1 / (t `2) < 1 & - 1 < ((t `1) / (t `2)) / (t `2) & ((t `1) / (t `2)) / (t `2) < 1 ) ; :: thesis: verum

end;

end;

end;

Out_In_Sq . t = |[(((t `1) / (t `2)) / (t `2)),(1 / (t `2))]| by A75, A103, Def1;
then ( p4 `2 = 1 / (t `2) & p4 `1 = ((t `1) / (t `2)) / (t `2) ) by EUCLID:56;
hence Out_In_Sq . t in K0 by A1, A105; :: thesis: verum

end;

end;

end;

hence Out_In_Sq . t in K0 ; :: thesis: verum

end;

A129: D = NonZero (TOP-REAL 2) by A1, SUBSET_1:def 5;
for x1, x2 being set st x1 in dom Out_In_Sq & x2 in dom Out_In_Sq & Out_In_Sq . x1 = Out_In_Sq . x2 holds
x1 = x2

proof

A130: { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) } c= D

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) } or x in D )
assume x in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) } ; :: thesis: x in D
then A131: ex p8 being Point of (TOP-REAL 2) st
( x = p8 & ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) ;
then not x in {(0. (TOP-REAL 2))} by TARSKI:def 1;
hence x in D by A3, A131, XBOOLE_0:def 5; :: thesis: verum

end;

A132: 1.REAL 2 <> 0. (TOP-REAL 2) by Lm1, REVROT_1:19;
( ( (1.REAL 2) `1 <= (1.REAL 2) `2 & - ((1.REAL 2) `2) <= (1.REAL 2) `1 ) or ( (1.REAL 2) `1 >= (1.REAL 2) `2 & (1.REAL 2) `1 <= - ((1.REAL 2) `2) ) ) by Th13;
then A133: 1.REAL 2 in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) } by A132;
the carrier of ((TOP-REAL 2) | D) = [#] ((TOP-REAL 2) | D)
.= D by PRE_TOPC:def 10 ;
then reconsider K11 = { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) } as non empty Subset of ((TOP-REAL 2) | D) by A133, A130;
reconsider K01 = { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `2 <= p8 `1 & - (p8 `1) <= p8 `2 ) or ( p8 `2 >= p8 `1 & p8 `2 <= - (p8 `1) ) ) & p8 <> 0. (TOP-REAL 2) ) } as non empty Subset of ((TOP-REAL 2) | D) by A2, Th27;
let x1, x2 be set ; :: thesis: ( x1 in dom Out_In_Sq & x2 in dom Out_In_Sq & Out_In_Sq . x1 = Out_In_Sq . x2 implies x1 = x2 )
assume that
A134: x1 in dom Out_In_Sq and
A135: x2 in dom Out_In_Sq and
A136: Out_In_Sq . x1 = Out_In_Sq . x2 ; :: thesis: x1 = x2
NonZero (TOP-REAL 2) <> {} by Th19;
then A137: dom Out_In_Sq = NonZero (TOP-REAL 2) by FUNCT_2:def 1;
then A138: x2 in D by A1, A135, SUBSET_1:def 5;
reconsider p1 = x1, p2 = x2 as Point of (TOP-REAL 2) by A134, A135, XBOOLE_0:def 5;
A139: D c= K01 \/ K11

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in D or x in K01 \/ K11 )
assume A140: x in D ; :: thesis: x in K01 \/ K11
then reconsider px = x as Point of (TOP-REAL 2) ;
not x in {(0. (TOP-REAL 2))} by A129, A140, XBOOLE_0:def 5;
then ( ( ( ( px `2 <= px `1 & - (px `1) <= px `2 ) or ( px `2 >= px `1 & px `2 <= - (px `1) ) ) & px <> 0. (TOP-REAL 2) ) or ( ( ( px `1 <= px `2 & - (px `2) <= px `1 ) or ( px `1 >= px `2 & px `1 <= - (px `2) ) ) & px <> 0. (TOP-REAL 2) ) ) by TARSKI:def 1, XREAL_1:27;
then ( x in K01 or x in K11 ) ;
hence x in K01 \/ K11 by XBOOLE_0:def 3; :: thesis: verum

end;

A141: x1 in D by A1, A134, A137, SUBSET_1:def 5;

now

per cases ( x1 in K01 or x1 in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) } ) by A139, A141, XBOOLE_0:def 3;

case x1 in K01 ; :: thesis: x1 = x2

then A142: ex p7 being Point of (TOP-REAL 2) st
( p1 = p7 & ( ( p7 `2 <= p7 `1 & - (p7 `1) <= p7 `2 ) or ( p7 `2 >= p7 `1 & p7 `2 <= - (p7 `1) ) ) & p7 <> 0. (TOP-REAL 2) ) ;
then A143: Out_In_Sq . p1 = |[(1 / (p1 `1)),(((p1 `2) / (p1 `1)) / (p1 `1))]| by Def1;

now

per cases ( x2 in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `2 <= p8 `1 & - (p8 `1) <= p8 `2 ) or ( p8 `2 >= p8 `1 & p8 `2 <= - (p8 `1) ) ) & p8 <> 0. (TOP-REAL 2) ) } or ( x2 in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) } & not x2 in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `2 <= p8 `1 & - (p8 `1) <= p8 `2 ) or ( p8 `2 >= p8 `1 & p8 `2 <= - (p8 `1) ) ) & p8 <> 0. (TOP-REAL 2) ) } ) ) by A139, A138, XBOOLE_0:def 3;

case x2 in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `2 <= p8 `1 & - (p8 `1) <= p8 `2 ) or ( p8 `2 >= p8 `1 & p8 `2 <= - (p8 `1) ) ) & p8 <> 0. (TOP-REAL 2) ) } ; :: thesis: x1 = x2

then ex p8 being Point of (TOP-REAL 2) st
( p2 = p8 & ( ( p8 `2 <= p8 `1 & - (p8 `1) <= p8 `2 ) or ( p8 `2 >= p8 `1 & p8 `2 <= - (p8 `1) ) ) & p8 <> 0. (TOP-REAL 2) ) ;
then A144: |[(1 / (p2 `1)),(((p2 `2) / (p2 `1)) / (p2 `1))]| = |[(1 / (p1 `1)),(((p1 `2) / (p1 `1)) / (p1 `1))]| by A136, A143, Def1;
A145: p1 = |[(p1 `1),(p1 `2)]| by EUCLID:57;
set qq = |[(1 / (p2 `1)),(((p2 `2) / (p2 `1)) / (p2 `1))]|;
A146: (1 / (p1 `1)) " = ((p1 `1) ") "
.= p1 `1 ;

A147: now

assume A148: p1 `1 = 0 ; :: thesis: contradiction
then p1 `2 = 0 by A142;
hence contradiction by A142, A148, EUCLID:57, EUCLID:58; :: thesis: verum

end;

|[(1 / (p2 `1)),(((p2 `2) / (p2 `1)) / (p2 `1))]| `1 = 1 / (p2 `1) by EUCLID:56;
then A149: 1 / (p1 `1) = 1 / (p2 `1) by A144, EUCLID:56;
|[(1 / (p2 `1)),(((p2 `2) / (p2 `1)) / (p2 `1))]| `2 = ((p2 `2) / (p2 `1)) / (p2 `1) by EUCLID:56;
then (p1 `2) / (p1 `1) = (p2 `2) / (p1 `1) by A144, A149, A146, A147, EUCLID:56, XCMPLX_1:53;
then p1 `2 = p2 `2 by A147, XCMPLX_1:53;
hence x1 = x2 by A149, A146, A145, EUCLID:57; :: thesis: verum

end;

case A150: ( x2 in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) } & not x2 in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `2 <= p8 `1 & - (p8 `1) <= p8 `2 ) or ( p8 `2 >= p8 `1 & p8 `2 <= - (p8 `1) ) ) & p8 <> 0. (TOP-REAL 2) ) } ) ; :: thesis: contradiction

A151: now

assume A152: p1 `1 = 0 ; :: thesis: contradiction
then p1 `2 = 0 by A142;
hence contradiction by A142, A152, EUCLID:57, EUCLID:58; :: thesis: verum

end;

A153: now

per cases ( ( p1 `2 <= p1 `1 & - (p1 `1) <= p1 `2 ) or ( p1 `2 >= p1 `1 & p1 `2 <= - (p1 `1) ) ) by A142;

case A154: ( p1 `2 <= p1 `1 & - (p1 `1) <= p1 `2 ) ; :: thesis: (p1 `2) / (p1 `1) <= 1

then p1 `1 >= 0 ;
then (p1 `2) / (p1 `1) <= (p1 `1) / (p1 `1) by A154, XREAL_1:74;
hence (p1 `2) / (p1 `1) <= 1 by A151, XCMPLX_1:60; :: thesis: verum

end;

case A155: ( p1 `2 >= p1 `1 & p1 `2 <= - (p1 `1) ) ; :: thesis: (p1 `2) / (p1 `1) <= 1

then p1 `1 <= 0 ;
then (p1 `2) / (p1 `1) <= (p1 `1) / (p1 `1) by A155, XREAL_1:75;
hence (p1 `2) / (p1 `1) <= 1 by A151, XCMPLX_1:60; :: thesis: verum

end;

end;

end;

A156: now

per cases ( ( p1 `2 <= p1 `1 & - (p1 `1) <= p1 `2 ) or ( p1 `2 >= p1 `1 & p1 `2 <= - (p1 `1) ) ) by A142;

case A157: ( p1 `2 <= p1 `1 & - (p1 `1) <= p1 `2 ) ; :: thesis: - 1 <= (p1 `2) / (p1 `1)

then p1 `1 >= 0 ;
then (- (p1 `1)) / (p1 `1) <= (p1 `2) / (p1 `1) by A157, XREAL_1:74;
hence - 1 <= (p1 `2) / (p1 `1) by A151, XCMPLX_1:198; :: thesis: verum

end;

case ( p1 `2 >= p1 `1 & p1 `2 <= - (p1 `1) ) ; :: thesis: - 1 <= (p1 `2) / (p1 `1)

then ( - (p1 `2) >= - (- (p1 `1)) & p1 `1 <= 0 ) by XREAL_1:26;
then (- (p1 `2)) / (- (p1 `1)) >= (p1 `1) / (- (p1 `1)) by XREAL_1:74;
then (- (p1 `2)) / (- (p1 `1)) >= - 1 by A151, XCMPLX_1:199;
hence - 1 <= (p1 `2) / (p1 `1) by XCMPLX_1:192; :: thesis: verum

end;

end;

end;

A158: ex p8 being Point of (TOP-REAL 2) st
( p2 = p8 & ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) by A150;

A159: now

assume A160: p2 `2 = 0 ; :: thesis: contradiction
then p2 `1 = 0 by A158;
hence contradiction by A158, A160, EUCLID:57, EUCLID:58; :: thesis: verum

end;

( ( not ( p2 `2 <= p2 `1 & - (p2 `1) <= p2 `2 ) & not ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1) ) ) or not p2 <> 0. (TOP-REAL 2) ) by A150;
then A161: Out_In_Sq . p2 = |[(((p2 `1) / (p2 `2)) / (p2 `2)),(1 / (p2 `2))]| by A158, Def1;
then ((p1 `2) / (p1 `1)) / (p1 `1) = 1 / (p2 `2) by A136, A143, SPPOL_2:1;
then A162: (p1 `2) / (p1 `1) = (1 / (p2 `2)) * (p1 `1) by A151, XCMPLX_1:88
.= (p1 `1) / (p2 `2) ;
1 / (p1 `1) = ((p2 `1) / (p2 `2)) / (p2 `2) by A136, A143, A161, SPPOL_2:1;
then A163: (p2 `1) / (p2 `2) = (1 / (p1 `1)) * (p2 `2) by A159, XCMPLX_1:88
.= (p2 `2) / (p1 `1) ;
then A164: ((p2 `1) / (p2 `2)) * ((p1 `2) / (p1 `1)) = 1 by A159, A151, A162, XCMPLX_1:113;
A165: (((p2 `1) / (p2 `2)) * ((p1 `2) / (p1 `1))) * (p1 `1) = 1 * (p1 `1) by A159, A151, A163, A162, XCMPLX_1:113;
then A166: p1 `2 <> 0 by A151;
A167: ex p9 being Point of (TOP-REAL 2) st
( p2 = p9 & ( ( p9 `1 <= p9 `2 & - (p9 `2) <= p9 `1 ) or ( p9 `1 >= p9 `2 & p9 `1 <= - (p9 `2) ) ) & p9 <> 0. (TOP-REAL 2) ) by A150;

A168: now

per cases ( ( p2 `1 <= p2 `2 & - (p2 `2) <= p2 `1 ) or ( p2 `1 >= p2 `2 & p2 `1 <= - (p2 `2) ) ) by A167;

case A169: ( p2 `1 <= p2 `2 & - (p2 `2) <= p2 `1 ) ; :: thesis: - 1 <= (p2 `1) / (p2 `2)

then p2 `2 >= 0 ;
then (- (p2 `2)) / (p2 `2) <= (p2 `1) / (p2 `2) by A169, XREAL_1:74;
hence - 1 <= (p2 `1) / (p2 `2) by A159, XCMPLX_1:198; :: thesis: verum

end;

case ( p2 `1 >= p2 `2 & p2 `1 <= - (p2 `2) ) ; :: thesis: - 1 <= (p2 `1) / (p2 `2)

then ( - (p2 `1) >= - (- (p2 `2)) & p2 `2 <= 0 ) by XREAL_1:26;
then (- (p2 `1)) / (- (p2 `2)) >= (p2 `2) / (- (p2 `2)) by XREAL_1:74;
then (- (p2 `1)) / (- (p2 `2)) >= - 1 by A159, XCMPLX_1:199;
hence - 1 <= (p2 `1) / (p2 `2) by XCMPLX_1:192; :: thesis: verum

end;

end;

end;

((p2 `1) / (p2 `2)) * (((p1 `2) / (p1 `1)) * (p1 `1)) = p1 `1 by A165;
then A170: ((p2 `1) / (p2 `2)) * (p1 `2) = p1 `1 by A151, XCMPLX_1:88;
then A171: (p2 `1) / (p2 `2) = (p1 `1) / (p1 `2) by A166, XCMPLX_1:90;

A172: now

per cases ( ( p2 `1 <= p2 `2 & - (p2 `2) <= p2 `1 ) or ( p2 `1 >= p2 `2 & p2 `1 <= - (p2 `2) ) ) by A167;

case A173: ( p2 `1 <= p2 `2 & - (p2 `2) <= p2 `1 ) ; :: thesis: (p2 `1) / (p2 `2) <= 1

then p2 `2 >= 0 ;
then (p2 `1) / (p2 `2) <= (p2 `2) / (p2 `2) by A173, XREAL_1:74;
hence (p2 `1) / (p2 `2) <= 1 by A159, XCMPLX_1:60; :: thesis: verum

end;

case A174: ( p2 `1 >= p2 `2 & p2 `1 <= - (p2 `2) ) ; :: thesis: (p2 `1) / (p2 `2) <= 1

then p2 `2 <= 0 ;
then (p2 `1) / (p2 `2) <= (p2 `2) / (p2 `2) by A174, XREAL_1:75;
hence (p2 `1) / (p2 `2) <= 1 by A159, XCMPLX_1:60; :: thesis: verum

end;

end;

end;

now

per cases ( 0 <= (p2 `1) / (p2 `2) or 0 > (p2 `1) / (p2 `2) ) ;

case 0 <= (p2 `1) / (p2 `2) ; :: thesis: contradiction

then A175: ( ( p1 `2 > 0 & p1 `1 >= 0 ) or ( p1 `2 < 0 & p1 `1 <= 0 ) ) by A151, A170;

now

assume (p1 `2) / (p1 `1) <> 1 ; :: thesis: contradiction
then (p1 `2) / (p1 `1) < 1 by A153, XXREAL_0:1;
hence contradiction by A164, A172, A175, XREAL_1:164; :: thesis: verum

end;

then p1 `2 = 1 * (p1 `1) by A151, XCMPLX_1:88;
then ((p2 `1) / (p2 `2)) * (p2 `2) = 1 * (p2 `2) by A151, A171, XCMPLX_1:60
.= p2 `2 ;
then p2 `1 = p2 `2 by A159, XCMPLX_1:88;
hence contradiction by A150, A167; :: thesis: verum

end;

case 0 > (p2 `1) / (p2 `2) ; :: thesis: contradiction

then A176: ( ( p1 `2 < 0 & p1 `1 > 0 ) or ( p1 `2 > 0 & p1 `1 < 0 ) ) by A171, XREAL_1:145;

now

assume (p1 `2) / (p1 `1) <> - 1 ; :: thesis: contradiction
then - 1 < (p1 `2) / (p1 `1) by A156, XXREAL_0:1;
hence contradiction by A164, A168, A176, XREAL_1:168; :: thesis: verum

end;

then p1 `2 = (- 1) * (p1 `1) by A151, XCMPLX_1:88
.= - (p1 `1) ;
then - (p1 `2) = p1 `1 ;
then (p2 `1) / (p2 `2) = - 1 by A166, A171, XCMPLX_1:198;
then p2 `1 = (- 1) * (p2 `2) by A159, XCMPLX_1:88;
then - (p2 `1) = p2 `2 ;
hence contradiction by A150, A167; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

case x1 in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) } ; :: thesis: x1 = x2

then A177: ex p7 being Point of (TOP-REAL 2) st
( p1 = p7 & ( ( p7 `1 <= p7 `2 & - (p7 `2) <= p7 `1 ) or ( p7 `1 >= p7 `2 & p7 `1 <= - (p7 `2) ) ) & p7 <> 0. (TOP-REAL 2) ) ;
then A178: Out_In_Sq . p1 = |[(((p1 `1) / (p1 `2)) / (p1 `2)),(1 / (p1 `2))]| by Th24;

now

per cases ( x2 in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) } or ( x2 in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `2 <= p8 `1 & - (p8 `1) <= p8 `2 ) or ( p8 `2 >= p8 `1 & p8 `2 <= - (p8 `1) ) ) & p8 <> 0. (TOP-REAL 2) ) } & not x2 in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) } ) ) by A139, A138, XBOOLE_0:def 3;

case x2 in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) } ; :: thesis: x1 = x2

then ex p8 being Point of (TOP-REAL 2) st
( p2 = p8 & ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) ;
then A179: |[(((p2 `1) / (p2 `2)) / (p2 `2)),(1 / (p2 `2))]| = |[(((p1 `1) / (p1 `2)) / (p1 `2)),(1 / (p1 `2))]| by A136, A178, Th24;
A180: p1 = |[(p1 `1),(p1 `2)]| by EUCLID:57;
set qq = |[(((p2 `1) / (p2 `2)) / (p2 `2)),(1 / (p2 `2))]|;
A181: (1 / (p1 `2)) " = ((p1 `2) ") "
.= p1 `2 ;

A182: now

assume A183: p1 `2 = 0 ; :: thesis: contradiction
then p1 `1 = 0 by A177;
hence contradiction by A177, A183, EUCLID:57, EUCLID:58; :: thesis: verum

end;

|[(((p2 `1) / (p2 `2)) / (p2 `2)),(1 / (p2 `2))]| `2 = 1 / (p2 `2) by EUCLID:56;
then A184: 1 / (p1 `2) = 1 / (p2 `2) by A179, EUCLID:56;
|[(((p2 `1) / (p2 `2)) / (p2 `2)),(1 / (p2 `2))]| `1 = ((p2 `1) / (p2 `2)) / (p2 `2) by EUCLID:56;
then (p1 `1) / (p1 `2) = (p2 `1) / (p1 `2) by A179, A184, A181, A182, EUCLID:56, XCMPLX_1:53;
then p1 `1 = p2 `1 by A182, XCMPLX_1:53;
hence x1 = x2 by A184, A181, A180, EUCLID:57; :: thesis: verum

end;

case A185: ( x2 in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `2 <= p8 `1 & - (p8 `1) <= p8 `2 ) or ( p8 `2 >= p8 `1 & p8 `2 <= - (p8 `1) ) ) & p8 <> 0. (TOP-REAL 2) ) } & not x2 in { p8 where p8 is Point of (TOP-REAL 2) : ( ( ( p8 `1 <= p8 `2 & - (p8 `2) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2) ) ) & p8 <> 0. (TOP-REAL 2) ) } ) ; :: thesis: contradiction

A186: now

assume A187: p1 `2 = 0 ; :: thesis: contradiction
then p1 `1 = 0 by A177;
hence contradiction by A177, A187, EUCLID:57, EUCLID:58; :: thesis: verum

end;

A188: now

per cases ( ( p1 `1 <= p1 `2 & - (p1 `2) <= p1 `1 ) or ( p1 `1 >= p1 `2 & p1 `1 <= - (p1 `2) ) ) by A177;

case A189: ( p1 `1 <= p1 `2 & - (p1 `2) <= p1 `1 ) ; :: thesis: (p1 `1) / (p1 `2) <= 1

then p1 `2 >= 0 ;
then (p1 `1) / (p1 `2) <= (p1 `2) / (p1 `2) by A189, XREAL_1:74;
hence (p1 `1) / (p1 `2) <= 1 by A186, XCMPLX_1:60; :: thesis: verum

end;

case A190: ( p1 `1 >= p1 `2 & p1 `1 <= - (p1 `2) ) ; :: thesis: (p1 `1) / (p1 `2) <= 1

then p1 `2 <= 0 ;
then (p1 `1) / (p1 `2) <= (p1 `2) / (p1 `2) by A190, XREAL_1:75;
hence (p1 `1) / (p1 `2) <= 1 by A186, XCMPLX_1:60; :: thesis: verum

end;

end;

end;

A191: now

per cases ( ( p1 `1 <= p1 `2 & - (p1 `2) <= p1 `1 ) or ( p1 `1 >= p1 `2 & p1 `1 <= - (p1 `2) ) ) by A177;

case A192: ( p1 `1 <= p1 `2 & - (p1 `2) <= p1 `1 ) ; :: thesis: - 1 <= (p1 `1) / (p1 `2)

then p1 `2 >= 0 ;
then (- (p1 `2)) / (p1 `2) <= (p1 `1) / (p1 `2) by A192, XREAL_1:74;
hence - 1 <= (p1 `1) / (p1 `2) by A186, XCMPLX_1:198; :: thesis: verum

end;

case ( p1 `1 >= p1 `2 & p1 `1 <= - (p1 `2) ) ; :: thesis: - 1 <= (p1 `1) / (p1 `2)

then ( - (p1 `1) >= - (- (p1 `2)) & p1 `2 <= 0 ) by XREAL_1:26;
then (- (p1 `1)) / (- (p1 `2)) >= (p1 `2) / (- (p1 `2)) by XREAL_1:74;
then (- (p1 `1)) / (- (p1 `2)) >= - 1 by A186, XCMPLX_1:199;
hence - 1 <= (p1 `1) / (p1 `2) by XCMPLX_1:192; :: thesis: verum

end;

end;

end;

A193: ex p8 being Point of (TOP-REAL 2) st
( p2 = p8 & ( ( p8 `2 <= p8 `1 & - (p8 `1) <= p8 `2 ) or ( p8 `2 >= p8 `1 & p8 `2 <= - (p8 `1) ) ) & p8 <> 0. (TOP-REAL 2) ) by A185;

A194: now

assume A195: p2 `1 = 0 ; :: thesis: contradiction
then p2 `2 = 0 by A193;
hence contradiction by A193, A195, EUCLID:57, EUCLID:58; :: thesis: verum

end;

A196: ex p9 being Point of (TOP-REAL 2) st
( p2 = p9 & ( ( p9 `2 <= p9 `1 & - (p9 `1) <= p9 `2 ) or ( p9 `2 >= p9 `1 & p9 `2 <= - (p9 `1) ) ) & p9 <> 0. (TOP-REAL 2) ) by A185;

A197: now

per cases ( ( p2 `2 <= p2 `1 & - (p2 `1) <= p2 `2 ) or ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1) ) ) by A196;

case A198: ( p2 `2 <= p2 `1 & - (p2 `1) <= p2 `2 ) ; :: thesis: - 1 <= (p2 `2) / (p2 `1)

then p2 `1 >= 0 ;
then (- (p2 `1)) / (p2 `1) <= (p2 `2) / (p2 `1) by A198, XREAL_1:74;
hence - 1 <= (p2 `2) / (p2 `1) by A194, XCMPLX_1:198; :: thesis: verum

end;

case ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1) ) ; :: thesis: - 1 <= (p2 `2) / (p2 `1)

then ( - (p2 `2) >= - (- (p2 `1)) & p2 `1 <= 0 ) by XREAL_1:26;
then (- (p2 `2)) / (- (p2 `1)) >= (p2 `1) / (- (p2 `1)) by XREAL_1:74;
then (- (p2 `2)) / (- (p2 `1)) >= - 1 by A194, XCMPLX_1:199;
hence - 1 <= (p2 `2) / (p2 `1) by XCMPLX_1:192; :: thesis: verum

end;

end;

end;

A199: Out_In_Sq . p2 = |[(1 / (p2 `1)),(((p2 `2) / (p2 `1)) / (p2 `1))]| by A193, Def1;
then 1 / (p1 `2) = ((p2 `2) / (p2 `1)) / (p2 `1) by A136, A178, SPPOL_2:1;
then A200: (p2 `2) / (p2 `1) = (1 / (p1 `2)) * (p2 `1) by A194, XCMPLX_1:88
.= (p2 `1) / (p1 `2) ;
((p1 `1) / (p1 `2)) / (p1 `2) = 1 / (p2 `1) by A136, A178, A199, SPPOL_2:1;
then (p1 `1) / (p1 `2) = (1 / (p2 `1)) * (p1 `2) by A186, XCMPLX_1:88
.= (p1 `2) / (p2 `1) ;
then A201: ((p2 `2) / (p2 `1)) * ((p1 `1) / (p1 `2)) = 1 by A194, A186, A200, XCMPLX_1:113;
then A202: p1 `1 <> 0 ;
(((p2 `2) / (p2 `1)) * ((p1 `1) / (p1 `2))) * (p1 `2) = p1 `2 by A201;
then ((p2 `2) / (p2 `1)) * (((p1 `1) / (p1 `2)) * (p1 `2)) = p1 `2 ;
then ((p2 `2) / (p2 `1)) * (p1 `1) = p1 `2 by A186, XCMPLX_1:88;
then A203: (p2 `2) / (p2 `1) = (p1 `2) / (p1 `1) by A202, XCMPLX_1:90;

A204: now

per cases ( ( p2 `2 <= p2 `1 & - (p2 `1) <= p2 `2 ) or ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1) ) ) by A196;

case A205: ( p2 `2 <= p2 `1 & - (p2 `1) <= p2 `2 ) ; :: thesis: (p2 `2) / (p2 `1) <= 1

then p2 `1 >= 0 ;
then (p2 `2) / (p2 `1) <= (p2 `1) / (p2 `1) by A205, XREAL_1:74;
hence (p2 `2) / (p2 `1) <= 1 by A194, XCMPLX_1:60; :: thesis: verum

end;

case A206: ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1) ) ; :: thesis: (p2 `2) / (p2 `1) <= 1

then p2 `1 <= 0 ;
then (p2 `2) / (p2 `1) <= (p2 `1) / (p2 `1) by A206, XREAL_1:75;
hence (p2 `2) / (p2 `1) <= 1 by A194, XCMPLX_1:60; :: thesis: verum

end;

end;

end;

now

per cases ( 0 <= (p2 `2) / (p2 `1) or 0 > (p2 `2) / (p2 `1) ) ;

case 0 <= (p2 `2) / (p2 `1) ; :: thesis: contradiction

then A207: ( ( p1 `1 > 0 & p1 `2 >= 0 ) or ( p1 `1 < 0 & p1 `2 <= 0 ) ) by A201, A202;

now

assume (p1 `1) / (p1 `2) <> 1 ; :: thesis: contradiction
then (p1 `1) / (p1 `2) < 1 by A188, XXREAL_0:1;
hence contradiction by A201, A204, A207, XREAL_1:164; :: thesis: verum

end;

then p1 `1 = 1 * (p1 `2) by A186, XCMPLX_1:88;
then ((p2 `2) / (p2 `1)) * (p2 `1) = 1 * (p2 `1) by A186, A203, XCMPLX_1:60
.= p2 `1 ;
then p2 `2 = p2 `1 by A194, XCMPLX_1:88;
hence contradiction by A185, A196; :: thesis: verum

end;

case 0 > (p2 `2) / (p2 `1) ; :: thesis: contradiction

then A208: ( ( p1 `1 < 0 & p1 `2 > 0 ) or ( p1 `1 > 0 & p1 `2 < 0 ) ) by A203, XREAL_1:145;

now

assume (p1 `1) / (p1 `2) <> - 1 ; :: thesis: contradiction
then - 1 < (p1 `1) / (p1 `2) by A191, XXREAL_0:1;
hence contradiction by A201, A197, A208, XREAL_1:168; :: thesis: verum

end;

then p1 `1 = (- 1) * (p1 `2) by A186, XCMPLX_1:88
.= - (p1 `2) ;
then - (p1 `1) = p1 `2 ;
then (p2 `2) / (p2 `1) = - 1 by A202, A203, XCMPLX_1:198;
then p2 `2 = (- 1) * (p2 `1) by A194, XCMPLX_1:88;
then - (p2 `2) = p2 `1 ;
hence contradiction by A185, A196; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: verum

end;

then A209: Out_In_Sq is one-to-one by FUNCT_1:def 8;
A210: for s being Point of (TOP-REAL 2) st s in Kb holds
Out_In_Sq . s = s

proof

let t be Point of (TOP-REAL 2); :: thesis: ( t in Kb implies Out_In_Sq . t = t )
assume t in Kb ; :: thesis: Out_In_Sq . t = t
then A211: ex p4 being Point of (TOP-REAL 2) st
( p4 = t & ( ( - 1 = p4 `1 & - 1 <= p4 `2 & p4 `2 <= 1 ) or ( p4 `1 = 1 & - 1 <= p4 `2 & p4 `2 <= 1 ) or ( - 1 = p4 `2 & - 1 <= p4 `1 & p4 `1 <= 1 ) or ( 1 = p4 `2 & - 1 <= p4 `1 & p4 `1 <= 1 ) ) ) by A1;
then A212: t <> 0. (TOP-REAL 2) by EUCLID:56, EUCLID:58;
A213: not t = 0. (TOP-REAL 2) by A211, EUCLID:56, EUCLID:58;

now

per cases ( ( t `2 <= t `1 & - (t `1) <= t `2 ) or ( t `2 >= t `1 & t `2 <= - (t `1) ) or ( not ( t `2 <= t `1 & - (t `1) <= t `2 ) & not ( t `2 >= t `1 & t `2 <= - (t `1) ) ) ) ;

case A214: ( ( t `2 <= t `1 & - (t `1) <= t `2 ) or ( t `2 >= t `1 & t `2 <= - (t `1) ) ) ; :: thesis: Out_In_Sq . t = t

then A215: Out_In_Sq . t = |[(1 / (t `1)),(((t `2) / (t `1)) / (t `1))]| by A213, Def1;
A216: ( ( 1 <= t `1 & t `1 >= - 1 ) or ( 1 >= t `1 & - 1 >= - (- (t `1)) ) ) by A211, A214, XREAL_1:26;

now

per cases ( t `1 = 1 or t `1 = - 1 ) by A211, A216, XXREAL_0:1;

case t `1 = 1 ; :: thesis: Out_In_Sq . t = t

hence Out_In_Sq . t = t by A215, EUCLID:57; :: thesis: verum

end;

case t `1 = - 1 ; :: thesis: Out_In_Sq . t = t

hence Out_In_Sq . t = t by A215, EUCLID:57; :: thesis: verum

end;

end;

end;

hence Out_In_Sq . t = t ; :: thesis: verum

end;

case A217: ( not ( t `2 <= t `1 & - (t `1) <= t `2 ) & not ( t `2 >= t `1 & t `2 <= - (t `1) ) ) ; :: thesis: Out_In_Sq . t = t

then A218: Out_In_Sq . t = |[(((t `1) / (t `2)) / (t `2)),(1 / (t `2))]| by A212, Def1;

now

per cases ( t `2 = 1 or t `2 = - 1 ) by A211, A217;

case t `2 = 1 ; :: thesis: Out_In_Sq . t = t

hence Out_In_Sq . t = t by A218, EUCLID:57; :: thesis: verum

end;

case t `2 = - 1 ; :: thesis: Out_In_Sq . t = t

hence Out_In_Sq . t = t by A218, EUCLID:57; :: thesis: verum

end;

end;

end;

hence Out_In_Sq . t = t ; :: thesis: verum

end;

end;

end;

hence Out_In_Sq . t = t ; :: thesis: verum

end;

ex h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) st
( h = Out_In_Sq & h is continuous ) by A2, Th50;
hence ex f being Function of ((TOP-REAL 2) | (B `)),((TOP-REAL 2) | (B `)) st
( f is continuous & f is one-to-one & ( for t being Point of (TOP-REAL 2) st t in K0 & t <> 0. (TOP-REAL 2) holds
not f . t in K0 \/ Kb ) & ( for r being Point of (TOP-REAL 2) st not r in K0 \/ Kb holds
f . r in K0 ) & ( for s being Point of (TOP-REAL 2) st s in Kb holds
f . s = s ) ) by A209, A4, A72, A210; :: thesis: verum