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 Th9;
A2: D ` = {(0. (TOP-REAL 2))} by A1;
A3: B ` = NonZero (TOP-REAL 2) by A1, SUBSET_1:def 4;
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 :: thesis: not Out_In_Sq . t in K0 \/ Kb

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

now :: thesis: ( ( Out_In_Sq . t in K0 & contradiction ) or ( Out_In_Sq . t in Kb & contradiction ) )

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 :: thesis: ( ( ( ( t `2 <= t `1 & - (t `1) <= t `2 ) or ( t `2 >= t `1 & t `2 <= - (t `1) ) ) & contradiction ) or ( not ( t `2 <= t `1 & - (t `1) <= t `2 ) & not ( t `2 >= t `1 & t `2 <= - (t `1) ) & contradiction ) )

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:52;

now :: thesis: ( ( t `1 >= 0 & contradiction ) or ( t `1 < 0 & contradiction ) )

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

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

now :: thesis: ( ( t `1 > 0 & contradiction ) or ( t `1 = 0 & contradiction ) )

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:68;
hence contradiction by A7, A17, XCMPLX_1:87; :: thesis: verum

end;

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

then t `2 = 0 by A14;
hence contradiction by A6, A18, EUCLID:53, EUCLID:54; :: 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:69;
then (- 1) * (t `1) > 1 by A19, XCMPLX_1:87;
then - (- (t `1)) <= - 1 by XREAL_1:24;
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:52;

now :: thesis: ( ( t `2 >= 0 & contradiction ) or ( t `2 < 0 & contradiction ) )

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

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

now :: thesis: ( ( t `2 > 0 & contradiction ) or ( t `2 = 0 & contradiction ) )

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:68;
hence contradiction by A7, A23, XCMPLX_1:87; :: 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:69;
then (- 1) * (t `2) > 1 by A24, XCMPLX_1:87;
then - (- (t `2)) <= - 1 by XREAL_1:24;
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 :: thesis: ( ( ( ( t `2 <= t `1 & - (t `1) <= t `2 ) or ( t `2 >= t `1 & t `2 <= - (t `1) ) ) & contradiction ) or ( not ( t `2 <= t `1 & - (t `1) <= t `2 ) & not ( t `2 >= t `1 & t `2 <= - (t `1) ) & contradiction ) )

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:52;

now :: thesis: ( ( - 1 = p4 `1 & - 1 <= p4 `2 & p4 `2 <= 1 & contradiction ) or ( p4 `1 = 1 & - 1 <= p4 `2 & p4 `2 <= 1 & contradiction ) or ( - 1 = p4 `2 & - 1 <= p4 `1 & p4 `1 <= 1 & contradiction ) or ( 1 = p4 `2 & - 1 <= p4 `1 & p4 `1 <= 1 & contradiction ) )

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 :: thesis: ( ( t `1 <> 0 & contradiction ) or ( t `1 = 0 & contradiction ) )

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:53, EUCLID:54; :: 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 :: thesis: ( ( t `1 <> 0 & contradiction ) or ( t `1 = 0 & contradiction ) )

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:53, EUCLID:54; :: 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, Th17;
A35: the carrier of (((TOP-REAL 2) | D) | K01) = [#] (((TOP-REAL 2) | D) | K01)
.= K01 by PRE_TOPC:def 5 ;
A36: dom (Out_In_Sq | K01) = (dom Out_In_Sq) /\ K01 by RELAT_1:61
.= D /\ K01 by A3, FUNCT_2:def 1
.= ([#] ((TOP-REAL 2) | D)) /\ K01 by PRE_TOPC:def 5
.= 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:3;
rng (Out_In_Sq | K01) c= the carrier of (((TOP-REAL 2) | D) | K01) by Th15;
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:49;
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 :: thesis: ( ( p4 `1 >= 1 & contradiction ) or ( - 1 >= p4 `1 & contradiction ) )

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

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:52; :: 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:52; :: 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, Th17;
t in K01 by A6, A27;
then A43: Out_In_Sq . t = (Out_In_Sq | K01) . t by FUNCT_1:49;
dom (Out_In_Sq | K01) = (dom Out_In_Sq) /\ K01 by RELAT_1:61
.= D /\ K01 by A3, FUNCT_2:def 1
.= ([#] ((TOP-REAL 2) | D)) /\ K01 by PRE_TOPC:def 5
.= 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:3;
rng (Out_In_Sq | K01) c= the carrier of (((TOP-REAL 2) | D) | K01) by Th15;
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 5 ;
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 :: thesis: ( ( p4 `1 >= 1 & contradiction ) or ( - 1 >= p4 `1 & contradiction ) )

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

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:52; :: 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:52; :: 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:52;

now :: thesis: ( ( - 1 = p4 `2 & - 1 <= p4 `1 & p4 `1 <= 1 & contradiction ) or ( p4 `2 = 1 & - 1 <= p4 `1 & p4 `1 <= 1 & contradiction ) or ( - 1 = p4 `1 & - 1 <= p4 `2 & p4 `2 <= 1 & contradiction ) or ( 1 = p4 `1 & - 1 <= p4 `2 & p4 `2 <= 1 & contradiction ) )

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 :: thesis: ( ( t `2 <> 0 & contradiction ) or ( t `2 = 0 & contradiction ) )

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 :: thesis: ( ( t `2 <> 0 & contradiction ) or ( t `2 = 0 & contradiction ) )

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, Th18;
A55: dom (Out_In_Sq | K11) = (dom Out_In_Sq) /\ K11 by RELAT_1:61
.= D /\ K11 by A3, FUNCT_2:def 1
.= ([#] ((TOP-REAL 2) | D)) /\ K11 by PRE_TOPC:def 5
.= 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, Th13;
then t in K11 by A6;
then A57: Out_In_Sq . t = (Out_In_Sq | K11) . t by FUNCT_1:49;
t in K11 by A6, A56;
then A58: (Out_In_Sq | K11) . t in rng (Out_In_Sq | K11) by A55, FUNCT_1:3;
rng (Out_In_Sq | K11) c= the carrier of (((TOP-REAL 2) | D) | K11) by Th16;
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 5 ;
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 :: thesis: ( ( p4 `2 >= 1 & contradiction ) or ( - 1 >= p4 `2 & contradiction ) )

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

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:52; :: 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:52; :: 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, Th18;
A64: the carrier of (((TOP-REAL 2) | D) | K11) = [#] (((TOP-REAL 2) | D) | K11)
.= K11 by PRE_TOPC:def 5 ;
A65: dom (Out_In_Sq | K11) = (dom Out_In_Sq) /\ K11 by RELAT_1:61
.= D /\ K11 by A3, FUNCT_2:def 1
.= ([#] ((TOP-REAL 2) | D)) /\ K11 by PRE_TOPC:def 5
.= 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, Th13;
then t in K11 by A6;
then A67: (Out_In_Sq | K11) . t in rng (Out_In_Sq | K11) by A65, FUNCT_1:3;
rng (Out_In_Sq | K11) c= the carrier of (((TOP-REAL 2) | D) | K11) by Th16;
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:49;
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 :: thesis: ( ( p4 `2 >= 1 & contradiction ) or ( - 1 >= p4 `2 & contradiction ) )

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

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:52; :: 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:52; :: 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, Th3;
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:5;
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 :: thesis: ( ( ( ( t `2 <= t `1 & - (t `1) <= t `2 ) or ( t `2 >= t `1 & t `2 <= - (t `1) ) ) & Out_In_Sq . t in K0 ) or ( not ( t `2 <= t `1 & - (t `1) <= t `2 ) & not ( t `2 >= t `1 & t `2 <= - (t `1) ) & Out_In_Sq . t in K0 ) )

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 :: thesis: ( ( t `1 > 0 & - 1 < 1 / (t `1) & 1 / (t `1) < 1 & - 1 < ((t `2) / (t `1)) / (t `1) & ((t `2) / (t `1)) / (t `1) < 1 ) or ( t `1 <= 0 & - 1 < 1 / (t `1) & 1 / (t `1) < 1 & - 1 < ((t `2) / (t `1)) / (t `1) & ((t `2) / (t `1)) / (t `1) < 1 ) )

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 :: thesis: ( ( t `2 > 0 & - 1 < 1 / (t `1) & 1 / (t `1) < 1 & - 1 < ((t `2) / (t `1)) / (t `1) & ((t `2) / (t `1)) / (t `1) < 1 ) or ( t `2 <= 0 & - 1 < 1 / (t `1) & 1 / (t `1) < 1 & - 1 < ((t `2) / (t `1)) / (t `1) & ((t `2) / (t `1)) / (t `1) < 1 ) )

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:14;
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:74;
then (t `2) / (t `1) < t `1 by A79, XCMPLX_1:89;
then A83: ((t `2) / (t `1)) / (t `1) < (t `1) / (t `1) by A79, XREAL_1:74;
0 < (t `2) / (t `1) by A79, A80, XREAL_1:139;
then A84: ((- 1) * (t `1)) / (t `1) < ((t `2) / (t `1)) / (t `1) by A79, XREAL_1:74;
(t `1) / (t `1) > 1 / (t `1) by A82, XREAL_1:74;
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:89; :: 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 :: thesis: ( t `1 < 1 implies t `1 >= 1 )

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:24; :: 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:14;
- (- (t `1)) >= - (t `2) by A77, A79, XREAL_1:24;
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:74;
then t `1 > - ((t `2) / (t `1)) by A79, XCMPLX_1:89;
then - (t `1) < - (- ((t `2) / (t `1))) by XREAL_1:24;
then A89: ((- 1) * (t `1)) / (t `1) < ((t `2) / (t `1)) / (t `1) by A79, XREAL_1:74;
(t `1) / (t `1) > 1 / (t `1) by A87, XREAL_1:74;
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:89; :: 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 :: thesis: ( ( t `1 = 0 & contradiction ) or ( t `1 < 0 & - 1 < 1 / (t `1) & 1 / (t `1) < 1 & - 1 < ((t `2) / (t `1)) / (t `1) & ((t `2) / (t `1)) / (t `1) < 1 ) )

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 :: thesis: ( ( t `2 > 0 & - 1 < 1 / (t `1) & 1 / (t `1) < 1 & - 1 < ((t `2) / (t `1)) / (t `1) & ((t `2) / (t `1)) / (t `1) < 1 ) or ( t `2 <= 0 & - 1 < 1 / (t `1) & 1 / (t `1) < 1 & - 1 < ((t `2) / (t `1)) / (t `1) & ((t `2) / (t `1)) / (t `1) < 1 ) )

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:24;
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:75;
then A96: - ((t `1) / (t `1)) < - ((- 1) / (t `1)) by XREAL_1:24;
- (t `1) < (t `1) ^2 by A95, SQUARE_1:46;
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:75;
then (t `2) / (t `1) > t `1 by A92, XCMPLX_1:89;
then A97: ((t `2) / (t `1)) / (t `1) < (t `1) / (t `1) by A92, XREAL_1:75;
0 > (t `2) / (t `1) by A92, A93, XREAL_1:142;
then ((- 1) * (t `1)) / (t `1) < ((t `2) / (t `1)) / (t `1) by A92, XREAL_1:75;
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:46;
t `1 <= t `2 by A77, A92;
then - (t `1) >= - (t `2) by XREAL_1:24;
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:75;
then t `1 < - ((t `2) / (t `1)) by A92, XCMPLX_1:89;
then - (t `1) > - (- ((t `2) / (t `1))) by XREAL_1:24;
then A102: ((- 1) * (t `1)) / (t `1) < ((t `2) / (t `1)) / (t `1) by A92, XREAL_1:75;
(t `1) / (t `1) > (- 1) / (t `1) by A100, XREAL_1:75;
then 1 > (- 1) / (t `1) by A92, XCMPLX_1:60;
then - 1 < - ((- 1) / (t `1)) by XREAL_1:24;
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:89; :: 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:52;
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 Th13;

A105: now :: thesis: ( ( t `2 > 0 & - 1 < 1 / (t `2) & 1 / (t `2) < 1 & - 1 < ((t `1) / (t `2)) / (t `2) & ((t `1) / (t `2)) / (t `2) < 1 ) or ( t `2 <= 0 & - 1 < 1 / (t `2) & 1 / (t `2) < 1 & - 1 < ((t `1) / (t `2)) / (t `2) & ((t `1) / (t `2)) / (t `2) < 1 ) )

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 :: thesis: ( ( t `1 > 0 & - 1 < 1 / (t `2) & 1 / (t `2) < 1 & - 1 < ((t `1) / (t `2)) / (t `2) & ((t `1) / (t `2)) / (t `2) < 1 ) or ( t `1 <= 0 & - 1 < 1 / (t `2) & 1 / (t `2) < 1 & - 1 < ((t `1) / (t `2)) / (t `2) & ((t `1) / (t `2)) / (t `2) < 1 ) )

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:14;
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:74;
then (t `1) / (t `2) < t `2 by A106, XCMPLX_1:89;
then A110: ((t `1) / (t `2)) / (t `2) < (t `2) / (t `2) by A106, XREAL_1:74;
0 < (t `1) / (t `2) by A106, A107, XREAL_1:139;
then A111: ((- 1) * (t `2)) / (t `2) < ((t `1) / (t `2)) / (t `2) by A106, XREAL_1:74;
(t `2) / (t `2) > 1 / (t `2) by A109, XREAL_1:74;
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:89; :: 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 :: thesis: ( t `2 < 1 implies t `2 >= 1 )

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:24; :: 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:14;
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:74;
then t `2 > - ((t `1) / (t `2)) by A106, XCMPLX_1:89;
then - (t `2) < - (- ((t `1) / (t `2))) by XREAL_1:24;
then A115: ((- 1) * (t `2)) / (t `2) < ((t `1) / (t `2)) / (t `2) by A106, XREAL_1:74;
(t `2) / (t `2) > 1 / (t `2) by A114, XREAL_1:74;
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:89; :: 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, Th13;

now :: thesis: ( ( t `1 > 0 & - 1 < 1 / (t `2) & 1 / (t `2) < 1 & - 1 < ((t `1) / (t `2)) / (t `2) & ((t `1) / (t `2)) / (t `2) < 1 ) or ( t `1 <= 0 & - 1 < 1 / (t `2) & 1 / (t `2) < 1 & - 1 < ((t `1) / (t `2)) / (t `2) & ((t `1) / (t `2)) / (t `2) < 1 ) )

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:24;
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:75;
then A122: - ((t `2) / (t `2)) < - ((- 1) / (t `2)) by XREAL_1:24;
- (t `2) < (t `2) ^2 by A121, SQUARE_1:46;
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:75;
then (t `1) / (t `2) > t `2 by A117, XCMPLX_1:89;
then A123: ((t `1) / (t `2)) / (t `2) < (t `2) / (t `2) by A117, XREAL_1:75;
0 > (t `1) / (t `2) by A117, A119, XREAL_1:142;
then ((- 1) * (t `2)) / (t `2) < ((t `1) / (t `2)) / (t `2) by A117, XREAL_1:75;
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:46;
- (t `2) >= - (t `1) by A103, A116, XREAL_1:24;
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:75;
then t `2 < - ((t `1) / (t `2)) by A117, XCMPLX_1:89;
then - (t `2) > - (- ((t `1) / (t `2))) by XREAL_1:24;
then A128: ((- 1) * (t `2)) / (t `2) < ((t `1) / (t `2)) / (t `2) by A117, XREAL_1:75;
(t `2) / (t `2) > (- 1) / (t `2) by A126, XREAL_1:75;
then 1 > (- 1) / (t `2) by A117, XCMPLX_1:60;
then - 1 < - ((- 1) / (t `2)) by XREAL_1:24;
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:89; :: 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:52;
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 4;
for x1, x2 being object 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 object ; :: 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 Th5;
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 5 ;
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, Th17;
let x1, x2 be object ; :: 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 Th9;
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 4;
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 object ; :: 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:25;
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 4;

now :: thesis: ( ( x1 in K01 & x1 = x2 ) 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) ) } & x1 = x2 ) )

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 :: thesis: ( ( 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) ) } & x1 = x2 ) 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) ) } & contradiction ) )

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:53;
set qq = |[(1 / (p2 `1)),(((p2 `2) / (p2 `1)) / (p2 `1))]|;
A146: (1 / (p1 `1)) " = ((p1 `1) ") "
.= p1 `1 ;

A147: now :: thesis: not p1 `1 = 0

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

end;

|[(1 / (p2 `1)),(((p2 `2) / (p2 `1)) / (p2 `1))]| `1 = 1 / (p2 `1) by EUCLID:52;
then A149: 1 / (p1 `1) = 1 / (p2 `1) by A144, EUCLID:52;
|[(1 / (p2 `1)),(((p2 `2) / (p2 `1)) / (p2 `1))]| `2 = ((p2 `2) / (p2 `1)) / (p2 `1) by EUCLID:52;
then (p1 `2) / (p1 `1) = (p2 `2) / (p1 `1) by A144, A149, A146, A147, EUCLID:52, XCMPLX_1:53;
then p1 `2 = p2 `2 by A147, XCMPLX_1:53;
hence x1 = x2 by A149, A146, A145, EUCLID:53; :: 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 :: thesis: not p1 `1 = 0

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

end;

A153: now :: thesis: ( ( p1 `2 <= p1 `1 & - (p1 `1) <= p1 `2 & (p1 `2) / (p1 `1) <= 1 ) or ( p1 `2 >= p1 `1 & p1 `2 <= - (p1 `1) & (p1 `2) / (p1 `1) <= 1 ) )

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) <= p1 `1 by XXREAL_0:2;
then p1 `1 >= 0 ;
then (p1 `2) / (p1 `1) <= (p1 `1) / (p1 `1) by A154, XREAL_1:72;
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) >= p1 `1 by XXREAL_0:2;
then p1 `1 <= 0 ;
then (p1 `2) / (p1 `1) <= (p1 `1) / (p1 `1) by A155, XREAL_1:73;
hence (p1 `2) / (p1 `1) <= 1 by A151, XCMPLX_1:60; :: thesis: verum

end;

end;

end;

A156: now :: thesis: ( ( p1 `2 <= p1 `1 & - (p1 `1) <= p1 `2 & - 1 <= (p1 `2) / (p1 `1) ) or ( p1 `2 >= p1 `1 & p1 `2 <= - (p1 `1) & - 1 <= (p1 `2) / (p1 `1) ) )

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) <= p1 `1 by XXREAL_0:2;
then p1 `1 >= 0 ;
then (- (p1 `1)) / (p1 `1) <= (p1 `2) / (p1 `1) by A157, XREAL_1:72;
hence - 1 <= (p1 `2) / (p1 `1) by A151, XCMPLX_1:197; :: thesis: verum

end;

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

( - (p1 `2) >= - (- (p1 `1)) & p1 `1 <= 0 ) by XREAL_1:24, A158;
then (- (p1 `2)) / (- (p1 `1)) >= (p1 `1) / (- (p1 `1)) by XREAL_1:72;
then (- (p1 `2)) / (- (p1 `1)) >= - 1 by A151, XCMPLX_1:198;
hence - 1 <= (p1 `2) / (p1 `1) by XCMPLX_1:191; :: thesis: verum

end;

end;

end;

A159: 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;

A160: now :: thesis: not p2 `2 = 0

assume A161: p2 `2 = 0 ; :: thesis: contradiction
then p2 `1 = 0 by A159;
hence contradiction by A159, A161, EUCLID:53, EUCLID:54; :: 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 A162: Out_In_Sq . p2 = |[(((p2 `1) / (p2 `2)) / (p2 `2)),(1 / (p2 `2))]| by A159, Def1;
then ((p1 `2) / (p1 `1)) / (p1 `1) = 1 / (p2 `2) by A136, A143, SPPOL_2:1;
then A163: (p1 `2) / (p1 `1) = (1 / (p2 `2)) * (p1 `1) by A151, XCMPLX_1:87
.= (p1 `1) / (p2 `2) ;
1 / (p1 `1) = ((p2 `1) / (p2 `2)) / (p2 `2) by A136, A143, A162, SPPOL_2:1;
then A164: (p2 `1) / (p2 `2) = (1 / (p1 `1)) * (p2 `2) by A160, XCMPLX_1:87
.= (p2 `2) / (p1 `1) ;
then A165: ((p2 `1) / (p2 `2)) * ((p1 `2) / (p1 `1)) = 1 by A160, A151, A163, XCMPLX_1:112;
A166: (((p2 `1) / (p2 `2)) * ((p1 `2) / (p1 `1))) * (p1 `1) = 1 * (p1 `1) by A160, A151, A164, A163, XCMPLX_1:112;
then A167: p1 `2 <> 0 by A151;
A168: 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;

A169: now :: thesis: ( ( p2 `1 <= p2 `2 & - (p2 `2) <= p2 `1 & - 1 <= (p2 `1) / (p2 `2) ) or ( p2 `1 >= p2 `2 & p2 `1 <= - (p2 `2) & - 1 <= (p2 `1) / (p2 `2) ) )

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

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

then - (p2 `2) <= p2 `2 by XXREAL_0:2;
then p2 `2 >= 0 ;
then (- (p2 `2)) / (p2 `2) <= (p2 `1) / (p2 `2) by A170, XREAL_1:72;
hence - 1 <= (p2 `1) / (p2 `2) by A160, XCMPLX_1:197; :: thesis: verum

end;

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

( - (p2 `1) >= - (- (p2 `2)) & p2 `2 <= 0 ) by XREAL_1:24, A171;
then (- (p2 `1)) / (- (p2 `2)) >= (p2 `2) / (- (p2 `2)) by XREAL_1:72;
then (- (p2 `1)) / (- (p2 `2)) >= - 1 by A160, XCMPLX_1:198;
hence - 1 <= (p2 `1) / (p2 `2) by XCMPLX_1:191; :: thesis: verum

end;

end;

end;

((p2 `1) / (p2 `2)) * (((p1 `2) / (p1 `1)) * (p1 `1)) = p1 `1 by A166;
then A172: ((p2 `1) / (p2 `2)) * (p1 `2) = p1 `1 by A151, XCMPLX_1:87;
then A173: (p2 `1) / (p2 `2) = (p1 `1) / (p1 `2) by A167, XCMPLX_1:89;

A174: now :: thesis: ( ( p2 `1 <= p2 `2 & - (p2 `2) <= p2 `1 & (p2 `1) / (p2 `2) <= 1 ) or ( p2 `1 >= p2 `2 & p2 `1 <= - (p2 `2) & (p2 `1) / (p2 `2) <= 1 ) )

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

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

then - (p2 `2) <= p2 `2 by XXREAL_0:2;
then p2 `2 >= 0 ;
then (p2 `1) / (p2 `2) <= (p2 `2) / (p2 `2) by A175, XREAL_1:72;
hence (p2 `1) / (p2 `2) <= 1 by A160, XCMPLX_1:60; :: thesis: verum

end;

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

then - (p2 `2) >= p2 `2 by XXREAL_0:2;
then p2 `2 <= 0 ;
then (p2 `1) / (p2 `2) <= (p2 `2) / (p2 `2) by A176, XREAL_1:73;
hence (p2 `1) / (p2 `2) <= 1 by A160, XCMPLX_1:60; :: thesis: verum

end;

end;

end;

now :: thesis: ( ( 0 <= (p2 `1) / (p2 `2) & contradiction ) or ( 0 > (p2 `1) / (p2 `2) & contradiction ) )

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

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

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

now :: thesis: not (p1 `2) / (p1 `1) <> 1

assume (p1 `2) / (p1 `1) <> 1 ; :: thesis: contradiction
then (p1 `2) / (p1 `1) < 1 by A153, XXREAL_0:1;
hence contradiction by A165, A174, A177, XREAL_1:162; :: thesis: verum

end;

then p1 `2 = 1 * (p1 `1) by A151, XCMPLX_1:87;
then ((p2 `1) / (p2 `2)) * (p2 `2) = 1 * (p2 `2) by A151, A173, XCMPLX_1:60
.= p2 `2 ;
then p2 `1 = p2 `2 by A160, XCMPLX_1:87;
hence contradiction by A150, A168; :: thesis: verum

end;

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

then A178: ( ( p1 `2 < 0 & p1 `1 > 0 ) or ( p1 `2 > 0 & p1 `1 < 0 ) ) by A173, XREAL_1:143;

now :: thesis: not (p1 `2) / (p1 `1) <> - 1

assume (p1 `2) / (p1 `1) <> - 1 ; :: thesis: contradiction
then - 1 < (p1 `2) / (p1 `1) by A156, XXREAL_0:1;
hence contradiction by A165, A169, A178, XREAL_1:166; :: thesis: verum

end;

then p1 `2 = (- 1) * (p1 `1) by A151, XCMPLX_1:87
.= - (p1 `1) ;
then - (p1 `2) = p1 `1 ;
then (p2 `1) / (p2 `2) = - 1 by A167, A173, XCMPLX_1:197;
then p2 `1 = (- 1) * (p2 `2) by A160, XCMPLX_1:87;
then - (p2 `1) = p2 `2 ;
hence contradiction by A150, A168; :: 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 A179: 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 A180: Out_In_Sq . p1 = |[(((p1 `1) / (p1 `2)) / (p1 `2)),(1 / (p1 `2))]| by Th14;

now :: thesis: ( ( 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) ) } & x1 = x2 ) 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) ) } & contradiction ) )

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 A181: |[(((p2 `1) / (p2 `2)) / (p2 `2)),(1 / (p2 `2))]| = |[(((p1 `1) / (p1 `2)) / (p1 `2)),(1 / (p1 `2))]| by A136, A180, Th14;
A182: p1 = |[(p1 `1),(p1 `2)]| by EUCLID:53;
set qq = |[(((p2 `1) / (p2 `2)) / (p2 `2)),(1 / (p2 `2))]|;
A183: (1 / (p1 `2)) " = ((p1 `2) ") "
.= p1 `2 ;

A184: now :: thesis: not p1 `2 = 0

assume A185: p1 `2 = 0 ; :: thesis: contradiction
then p1 `1 = 0 by A179;
hence contradiction by A179, A185, EUCLID:53, EUCLID:54; :: thesis: verum

end;

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

end;

case A187: ( 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

A188: now :: thesis: not p1 `2 = 0

assume A189: p1 `2 = 0 ; :: thesis: contradiction
then p1 `1 = 0 by A179;
hence contradiction by A179, A189, EUCLID:53, EUCLID:54; :: thesis: verum

end;

A190: now :: thesis: ( ( p1 `1 <= p1 `2 & - (p1 `2) <= p1 `1 & (p1 `1) / (p1 `2) <= 1 ) or ( p1 `1 >= p1 `2 & p1 `1 <= - (p1 `2) & (p1 `1) / (p1 `2) <= 1 ) )

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

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

then - (p1 `2) <= p1 `2 by XXREAL_0:2;
then p1 `2 >= 0 ;
then (p1 `1) / (p1 `2) <= (p1 `2) / (p1 `2) by A191, XREAL_1:72;
hence (p1 `1) / (p1 `2) <= 1 by A188, XCMPLX_1:60; :: thesis: verum

end;

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

then - (p1 `2) >= p1 `2 by XXREAL_0:2;
then p1 `2 <= 0 ;
then (p1 `1) / (p1 `2) <= (p1 `2) / (p1 `2) by A192, XREAL_1:73;
hence (p1 `1) / (p1 `2) <= 1 by A188, XCMPLX_1:60; :: thesis: verum

end;

end;

end;

A193: now :: thesis: ( ( p1 `1 <= p1 `2 & - (p1 `2) <= p1 `1 & - 1 <= (p1 `1) / (p1 `2) ) or ( p1 `1 >= p1 `2 & p1 `1 <= - (p1 `2) & - 1 <= (p1 `1) / (p1 `2) ) )

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

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

then - (p1 `2) <= p1 `2 by XXREAL_0:2;
then p1 `2 >= 0 ;
then (- (p1 `2)) / (p1 `2) <= (p1 `1) / (p1 `2) by A194, XREAL_1:72;
hence - 1 <= (p1 `1) / (p1 `2) by A188, XCMPLX_1:197; :: thesis: verum

end;

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

( - (p1 `1) >= - (- (p1 `2)) & p1 `2 <= 0 ) by XREAL_1:24, A195;
then (- (p1 `1)) / (- (p1 `2)) >= (p1 `2) / (- (p1 `2)) by XREAL_1:72;
then (- (p1 `1)) / (- (p1 `2)) >= - 1 by A188, XCMPLX_1:198;
hence - 1 <= (p1 `1) / (p1 `2) by XCMPLX_1:191; :: thesis: verum

end;

end;

end;

A196: 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 A187;

A197: now :: thesis: not p2 `1 = 0

assume A198: p2 `1 = 0 ; :: thesis: contradiction
then p2 `2 = 0 by A196;
hence contradiction by A196, A198, EUCLID:53, EUCLID:54; :: thesis: verum

end;

A199: 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 A187;

A200: now :: thesis: ( ( p2 `2 <= p2 `1 & - (p2 `1) <= p2 `2 & - 1 <= (p2 `2) / (p2 `1) ) or ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1) & - 1 <= (p2 `2) / (p2 `1) ) )

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

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

then - (p2 `1) <= p2 `1 by XXREAL_0:2;
then p2 `1 >= 0 ;
then (- (p2 `1)) / (p2 `1) <= (p2 `2) / (p2 `1) by A201, XREAL_1:72;
hence - 1 <= (p2 `2) / (p2 `1) by A197, XCMPLX_1:197; :: thesis: verum

end;

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

( - (p2 `2) >= - (- (p2 `1)) & p2 `1 <= 0 ) by XREAL_1:24, A202;
then (- (p2 `2)) / (- (p2 `1)) >= (p2 `1) / (- (p2 `1)) by XREAL_1:72;
then (- (p2 `2)) / (- (p2 `1)) >= - 1 by A197, XCMPLX_1:198;
hence - 1 <= (p2 `2) / (p2 `1) by XCMPLX_1:191; :: thesis: verum

end;

end;

end;

A203: Out_In_Sq . p2 = |[(1 / (p2 `1)),(((p2 `2) / (p2 `1)) / (p2 `1))]| by A196, Def1;
then 1 / (p1 `2) = ((p2 `2) / (p2 `1)) / (p2 `1) by A136, A180, SPPOL_2:1;
then A204: (p2 `2) / (p2 `1) = (1 / (p1 `2)) * (p2 `1) by A197, XCMPLX_1:87
.= (p2 `1) / (p1 `2) ;
((p1 `1) / (p1 `2)) / (p1 `2) = 1 / (p2 `1) by A136, A180, A203, SPPOL_2:1;
then (p1 `1) / (p1 `2) = (1 / (p2 `1)) * (p1 `2) by A188, XCMPLX_1:87
.= (p1 `2) / (p2 `1) ;
then A205: ((p2 `2) / (p2 `1)) * ((p1 `1) / (p1 `2)) = 1 by A197, A188, A204, XCMPLX_1:112;
then A206: p1 `1 <> 0 ;
(((p2 `2) / (p2 `1)) * ((p1 `1) / (p1 `2))) * (p1 `2) = p1 `2 by A205;
then ((p2 `2) / (p2 `1)) * (((p1 `1) / (p1 `2)) * (p1 `2)) = p1 `2 ;
then ((p2 `2) / (p2 `1)) * (p1 `1) = p1 `2 by A188, XCMPLX_1:87;
then A207: (p2 `2) / (p2 `1) = (p1 `2) / (p1 `1) by A206, XCMPLX_1:89;

A208: now :: thesis: ( ( p2 `2 <= p2 `1 & - (p2 `1) <= p2 `2 & (p2 `2) / (p2 `1) <= 1 ) or ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1) & (p2 `2) / (p2 `1) <= 1 ) )

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

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

then - (p2 `1) <= p2 `1 by XXREAL_0:2;
then p2 `1 >= 0 ;
then (p2 `2) / (p2 `1) <= (p2 `1) / (p2 `1) by A209, XREAL_1:72;
hence (p2 `2) / (p2 `1) <= 1 by A197, XCMPLX_1:60; :: thesis: verum

end;

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

then - (p2 `1) >= p2 `1 by XXREAL_0:2;
then p2 `1 <= 0 ;
then (p2 `2) / (p2 `1) <= (p2 `1) / (p2 `1) by A210, XREAL_1:73;
hence (p2 `2) / (p2 `1) <= 1 by A197, XCMPLX_1:60; :: thesis: verum

end;

end;

end;

now :: thesis: ( ( 0 <= (p2 `2) / (p2 `1) & contradiction ) or ( 0 > (p2 `2) / (p2 `1) & contradiction ) )

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

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

then A211: ( ( p1 `1 > 0 & p1 `2 >= 0 ) or ( p1 `1 < 0 & p1 `2 <= 0 ) ) by A205, A206;

now :: thesis: not (p1 `1) / (p1 `2) <> 1

assume (p1 `1) / (p1 `2) <> 1 ; :: thesis: contradiction
then (p1 `1) / (p1 `2) < 1 by A190, XXREAL_0:1;
hence contradiction by A205, A208, A211, XREAL_1:162; :: thesis: verum

end;

then p1 `1 = 1 * (p1 `2) by A188, XCMPLX_1:87;
then ((p2 `2) / (p2 `1)) * (p2 `1) = 1 * (p2 `1) by A188, A207, XCMPLX_1:60
.= p2 `1 ;
then p2 `2 = p2 `1 by A197, XCMPLX_1:87;
hence contradiction by A187, A199; :: thesis: verum

end;

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

then A212: ( ( p1 `1 < 0 & p1 `2 > 0 ) or ( p1 `1 > 0 & p1 `2 < 0 ) ) by A207, XREAL_1:143;

now :: thesis: not (p1 `1) / (p1 `2) <> - 1

assume (p1 `1) / (p1 `2) <> - 1 ; :: thesis: contradiction
then - 1 < (p1 `1) / (p1 `2) by A193, XXREAL_0:1;
hence contradiction by A205, A200, A212, XREAL_1:166; :: thesis: verum

end;

then p1 `1 = (- 1) * (p1 `2) by A188, XCMPLX_1:87
.= - (p1 `2) ;
then - (p1 `1) = p1 `2 ;
then (p2 `2) / (p2 `1) = - 1 by A206, A207, XCMPLX_1:197;
then p2 `2 = (- 1) * (p2 `1) by A197, XCMPLX_1:87;
then - (p2 `2) = p2 `1 ;
hence contradiction by A187, A199; :: 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 A213: Out_In_Sq is one-to-one by FUNCT_1:def 4;
A214: 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 A215: 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 A216: t <> 0. (TOP-REAL 2) by EUCLID:52, EUCLID:54;
A217: not t = 0. (TOP-REAL 2) by A215, EUCLID:52, EUCLID:54;

now :: thesis: ( ( ( ( t `2 <= t `1 & - (t `1) <= t `2 ) or ( t `2 >= t `1 & t `2 <= - (t `1) ) ) & Out_In_Sq . t = t ) or ( not ( t `2 <= t `1 & - (t `1) <= t `2 ) & not ( t `2 >= t `1 & t `2 <= - (t `1) ) & Out_In_Sq . t = t ) )

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 A218: ( ( t `2 <= t `1 & - (t `1) <= t `2 ) or ( t `2 >= t `1 & t `2 <= - (t `1) ) ) ; :: thesis: Out_In_Sq . t = t

then A219: Out_In_Sq . t = |[(1 / (t `1)),(((t `2) / (t `1)) / (t `1))]| by A217, Def1;
A220: ( ( 1 <= t `1 & t `1 >= - 1 ) or ( 1 >= t `1 & - 1 >= - (- (t `1)) ) ) by A215, A218, XREAL_1:24;

now :: thesis: ( ( t `1 = 1 & Out_In_Sq . t = t ) or ( t `1 = - 1 & Out_In_Sq . t = t ) )

per cases ( t `1 = 1 or t `1 = - 1 ) by A215, A220, XXREAL_0:1;

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

hence Out_In_Sq . t = t by A219, EUCLID:53; :: thesis: verum

end;

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

hence Out_In_Sq . t = t by A219, EUCLID:53; :: thesis: verum

end;

end;

end;

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

end;

case A221: ( 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 A222: Out_In_Sq . t = |[(((t `1) / (t `2)) / (t `2)),(1 / (t `2))]| by A216, Def1;

now :: thesis: ( ( t `2 = 1 & Out_In_Sq . t = t ) or ( t `2 = - 1 & Out_In_Sq . t = t ) )

per cases ( t `2 = 1 or t `2 = - 1 ) by A215, A221;

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

hence Out_In_Sq . t = t by A222, EUCLID:53; :: thesis: verum

end;

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

hence Out_In_Sq . t = t by A222, EUCLID:53; :: 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, Th40;
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 A213, A4, A72, A214; :: thesis: verum