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 A2: B ` = NonZero (TOP-REAL 2) by SUBSET_1:def 5;
reconsider D = B ` as non empty Subset of (TOP-REAL 2) by A1, Th19;
A3: D ` = {(0. (TOP-REAL 2))} by A1;
then consider h being Function of ((TOP-REAL 2) | D),((TOP-REAL 2) | D) such that
A4: ( h = Out_In_Sq & h is continuous ) by Th50;
A5: D = NonZero (TOP-REAL 2) by A1, SUBSET_1:def 5;
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) ) } ;
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) ) } ;
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

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
A6: ( x1 in dom Out_In_Sq & x2 in dom Out_In_Sq ) and
A7: Out_In_Sq . x1 = Out_In_Sq . x2 ; :: thesis: x1 = x2
NonZero (TOP-REAL 2) <> {} by Th19;
then A8: dom Out_In_Sq = NonZero (TOP-REAL 2) by FUNCT_2:def 1;
reconsider p1 = x1, p2 = x2 as Point of (TOP-REAL 2) by A6, XBOOLE_0:def 5;
A9: the carrier of ((TOP-REAL 2) | D) = [#] ((TOP-REAL 2) | D)
.= D by PRE_TOPC:def 10 ;
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 A3, Th27;
( ( ( (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 ) ) ) & 1.REAL 2 <> 0. (TOP-REAL 2) ) by Th13, REVROT_1:19, XX;
then A10: 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) ) } ;
{ 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 consider p8 being Point of (TOP-REAL 2) such that
A11: ( x = p8 & ( ( p8 `1 <= p8 `2 & - (p8 `2 ) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2 ) ) ) & p8 <> 0. (TOP-REAL 2) ) ;
not x in {(0. (TOP-REAL 2))} by A11, TARSKI:def 1;
hence x in D by A2, A11, XBOOLE_0:def 5; :: thesis: verum

end;

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 A9, A10;
A12: 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 A13: x in D ; :: thesis: x in K01 \/ K11
then A14: ( x in the carrier of (TOP-REAL 2) & not x in {(0. (TOP-REAL 2))} ) by A5, XBOOLE_0:def 5;
reconsider px = x as Point of (TOP-REAL 2) by A13;
( ( ( ( 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 A14, 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;

A15: ( x1 in D & x2 in D ) by A1, A6, A8, 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 A12, A15, XBOOLE_0:def 3;

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

then consider p7 being Point of (TOP-REAL 2) such that
A16: ( p1 = p7 & ( ( p7 `2 <= p7 `1 & - (p7 `1 ) <= p7 `2 ) or ( p7 `2 >= p7 `1 & p7 `2 <= - (p7 `1 ) ) ) & p7 <> 0. (TOP-REAL 2) ) ;
A17: Out_In_Sq . p1 = |[(1 / (p1 `1 )),(((p1 `2 ) / (p1 `1 )) / (p1 `1 ))]| by A16, 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 A12, A15, 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 consider p8 being Point of (TOP-REAL 2) such that
A18: ( p2 = p8 & ( ( p8 `2 <= p8 `1 & - (p8 `1 ) <= p8 `2 ) or ( p8 `2 >= p8 `1 & p8 `2 <= - (p8 `1 ) ) ) & p8 <> 0. (TOP-REAL 2) ) ;
A19: |[(1 / (p2 `1 )),(((p2 `2 ) / (p2 `1 )) / (p2 `1 ))]| = |[(1 / (p1 `1 )),(((p1 `2 ) / (p1 `1 )) / (p1 `1 ))]| by A7, A17, A18, Def1;
set qq = |[(1 / (p2 `1 )),(((p2 `2 ) / (p2 `1 )) / (p2 `1 ))]|;
( |[(1 / (p2 `1 )),(((p2 `2 ) / (p2 `1 )) / (p2 `1 ))]| `1 = 1 / (p2 `1 ) & |[(1 / (p2 `1 )),(((p2 `2 ) / (p2 `1 )) / (p2 `1 ))]| `2 = ((p2 `2 ) / (p2 `1 )) / (p2 `1 ) ) by EUCLID:56;
then A20: ( 1 / (p1 `1 ) = 1 / (p2 `1 ) & ((p1 `2 ) / (p1 `1 )) / (p1 `1 ) = ((p2 `2 ) / (p2 `1 )) / (p2 `1 ) ) by A19, EUCLID:56;
A21: (1 / (p1 `1 )) " = ((p1 `1 ) " ) "
.= p1 `1 ;

A23: now

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

end;

then (p1 `2 ) / (p1 `1 ) = (p2 `2 ) / (p1 `1 ) by A20, A21, XCMPLX_1:53;
then A25: p1 `2 = p2 `2 by A23, XCMPLX_1:53;
p1 = |[(p1 `1 ),(p1 `2 )]| by EUCLID:57;
hence x1 = x2 by A20, A21, A25, EUCLID:57; :: thesis: verum

end;

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

then consider p8 being Point of (TOP-REAL 2) such that
A27: ( p2 = p8 & ( ( p8 `1 <= p8 `2 & - (p8 `2 ) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2 ) ) ) & p8 <> 0. (TOP-REAL 2) ) ;
( ( 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 A26;
then Out_In_Sq . p2 = |[(((p2 `1 ) / (p2 `2 )) / (p2 `2 )),(1 / (p2 `2 ))]| by A27, Def1;
then A28: ( 1 / (p1 `1 ) = ((p2 `1 ) / (p2 `2 )) / (p2 `2 ) & ((p1 `2 ) / (p1 `1 )) / (p1 `1 ) = 1 / (p2 `2 ) ) by A7, A17, SPPOL_2:1;

A29: now

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

end;

A31: now

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

end;

A33: (p2 `1 ) / (p2 `2 ) = (1 / (p1 `1 )) * (p2 `2 ) by A28, A29, XCMPLX_1:88
.= (p2 `2 ) / (p1 `1 ) ;
A34: (p1 `2 ) / (p1 `1 ) = (1 / (p2 `2 )) * (p1 `1 ) by A28, A31, XCMPLX_1:88
.= (p1 `1 ) / (p2 `2 ) ;
then A35: ((p2 `1 ) / (p2 `2 )) * ((p1 `2 ) / (p1 `1 )) = 1 by A29, A31, A33, XCMPLX_1:113;
A36: (((p2 `1 ) / (p2 `2 )) * ((p1 `2 ) / (p1 `1 ))) * (p1 `1 ) = 1 * (p1 `1 ) by A29, A31, A33, A34, XCMPLX_1:113;
then ((p2 `1 ) / (p2 `2 )) * (((p1 `2 ) / (p1 `1 )) * (p1 `1 )) = p1 `1 ;
then A37: ((p2 `1 ) / (p2 `2 )) * (p1 `2 ) = p1 `1 by A31, XCMPLX_1:88;
A38: ( p2 `1 <> 0 & p1 `2 <> 0 ) by A31, A36;
then A39: (p2 `1 ) / (p2 `2 ) = (p1 `1 ) / (p1 `2 ) by A37, XCMPLX_1:90;
consider p9 being Point of (TOP-REAL 2) such that
A40: ( 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 A26;

A41: now

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

case A42: ( 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 A42, XREAL_1:74;
hence (p2 `1 ) / (p2 `2 ) <= 1 by A29, XCMPLX_1:60; :: thesis: verum

end;

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

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

end;

end;

end;

A45: now

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

case A46: ( 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 A46, XREAL_1:74;
hence (p1 `2 ) / (p1 `1 ) <= 1 by A31, XCMPLX_1:60; :: thesis: verum

end;

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

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

end;

end;

end;

A49: now

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

case A50: ( 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 A50, XREAL_1:74;
hence - 1 <= (p2 `1 ) / (p2 `2 ) by A29, XCMPLX_1:198; :: thesis: verum

end;

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

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

end;

end;

end;

A54: now

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

case A55: ( 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 A55, XREAL_1:74;
hence - 1 <= (p1 `2 ) / (p1 `1 ) by A31, XCMPLX_1:198; :: thesis: verum

end;

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

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

end;

end;

end;

now

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

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

then B60: ( ( p1 `2 > 0 & p1 `1 >= 0 ) or ( p1 `2 < 0 & p1 `1 <= 0 ) ) by A31, A37;

now

assume (p1 `2 ) / (p1 `1 ) <> 1 ; :: thesis: contradiction
then (p1 `2 ) / (p1 `1 ) < 1 by A45, XXREAL_0:1;
hence contradiction by A35, A41, A59, B60, XREAL_1:164; :: thesis: verum

end;

then p1 `2 = 1 * (p1 `1 ) by A31, XCMPLX_1:88;
then ((p2 `1 ) / (p2 `2 )) * (p2 `2 ) = 1 * (p2 `2 ) by A31, A39, XCMPLX_1:60
.= p2 `2 ;
then p2 `1 = p2 `2 by A29, XCMPLX_1:88;
hence contradiction by A26, A40; :: thesis: verum

end;

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

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

now

assume (p1 `2 ) / (p1 `1 ) <> - 1 ; :: thesis: contradiction
then - 1 < (p1 `2 ) / (p1 `1 ) by A54, XXREAL_0:1;
hence contradiction by A35, A49, A61, B62, XREAL_1:168; :: thesis: verum

end;

then p1 `2 = (- 1) * (p1 `1 ) by A31, XCMPLX_1:88
.= - (p1 `1 ) ;
then - (p1 `2 ) = p1 `1 ;
then (p2 `1 ) / (p2 `2 ) = - 1 by A38, A39, XCMPLX_1:198;
then p2 `1 = (- 1) * (p2 `2 ) by A29, XCMPLX_1:88;
then - (p2 `1 ) = p2 `2 ;
hence contradiction by A26, A40; :: 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 consider p7 being Point of (TOP-REAL 2) such that
A63: ( p1 = p7 & ( ( p7 `1 <= p7 `2 & - (p7 `2 ) <= p7 `1 ) or ( p7 `1 >= p7 `2 & p7 `1 <= - (p7 `2 ) ) ) & p7 <> 0. (TOP-REAL 2) ) ;
A64: Out_In_Sq . p1 = |[(((p1 `1 ) / (p1 `2 )) / (p1 `2 )),(1 / (p1 `2 ))]| by A63, 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 A12, A15, 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 consider p8 being Point of (TOP-REAL 2) such that
A65: ( p2 = p8 & ( ( p8 `1 <= p8 `2 & - (p8 `2 ) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2 ) ) ) & p8 <> 0. (TOP-REAL 2) ) ;
A66: |[(((p2 `1 ) / (p2 `2 )) / (p2 `2 )),(1 / (p2 `2 ))]| = |[(((p1 `1 ) / (p1 `2 )) / (p1 `2 )),(1 / (p1 `2 ))]| by A7, A64, A65, Th24;
set qq = |[(((p2 `1 ) / (p2 `2 )) / (p2 `2 )),(1 / (p2 `2 ))]|;
( |[(((p2 `1 ) / (p2 `2 )) / (p2 `2 )),(1 / (p2 `2 ))]| `2 = 1 / (p2 `2 ) & |[(((p2 `1 ) / (p2 `2 )) / (p2 `2 )),(1 / (p2 `2 ))]| `1 = ((p2 `1 ) / (p2 `2 )) / (p2 `2 ) ) by EUCLID:56;
then A67: ( 1 / (p1 `2 ) = 1 / (p2 `2 ) & ((p1 `1 ) / (p1 `2 )) / (p1 `2 ) = ((p2 `1 ) / (p2 `2 )) / (p2 `2 ) ) by A66, EUCLID:56;
A68: (1 / (p1 `2 )) " = ((p1 `2 ) " ) "
.= p1 `2 ;

A70: now

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

end;

then (p1 `1 ) / (p1 `2 ) = (p2 `1 ) / (p1 `2 ) by A67, A68, XCMPLX_1:53;
then A72: p1 `1 = p2 `1 by A70, XCMPLX_1:53;
p1 = |[(p1 `1 ),(p1 `2 )]| by EUCLID:57;
hence x1 = x2 by A67, A68, A72, EUCLID:57; :: thesis: verum

end;

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

then consider p8 being Point of (TOP-REAL 2) such that
A74: ( p2 = p8 & ( ( p8 `2 <= p8 `1 & - (p8 `1 ) <= p8 `2 ) or ( p8 `2 >= p8 `1 & p8 `2 <= - (p8 `1 ) ) ) & p8 <> 0. (TOP-REAL 2) ) ;
Out_In_Sq . p2 = |[(1 / (p2 `1 )),(((p2 `2 ) / (p2 `1 )) / (p2 `1 ))]| by A74, Def1;
then A75: ( 1 / (p1 `2 ) = ((p2 `2 ) / (p2 `1 )) / (p2 `1 ) & ((p1 `1 ) / (p1 `2 )) / (p1 `2 ) = 1 / (p2 `1 ) ) by A7, A64, SPPOL_2:1;

A76: now

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

end;

A78: now

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

end;

A80: (p2 `2 ) / (p2 `1 ) = (1 / (p1 `2 )) * (p2 `1 ) by A75, A76, XCMPLX_1:88
.= (p2 `1 ) / (p1 `2 ) ;
(p1 `1 ) / (p1 `2 ) = (1 / (p2 `1 )) * (p1 `2 ) by A75, A78, XCMPLX_1:88
.= (p1 `2 ) / (p2 `1 ) ;
then A81: ((p2 `2 ) / (p2 `1 )) * ((p1 `1 ) / (p1 `2 )) = 1 by A76, A78, A80, XCMPLX_1:113;
then (((p2 `2 ) / (p2 `1 )) * ((p1 `1 ) / (p1 `2 ))) * (p1 `2 ) = p1 `2 ;
then ((p2 `2 ) / (p2 `1 )) * (((p1 `1 ) / (p1 `2 )) * (p1 `2 )) = p1 `2 ;
then A82: ((p2 `2 ) / (p2 `1 )) * (p1 `1 ) = p1 `2 by A78, XCMPLX_1:88;
A83: ( p2 `2 <> 0 & p1 `1 <> 0 ) by A81;
then A84: (p2 `2 ) / (p2 `1 ) = (p1 `2 ) / (p1 `1 ) by A82, XCMPLX_1:90;
consider p9 being Point of (TOP-REAL 2) such that
A85: ( 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 A73;

A86: now

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

case A87: ( 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 A87, XREAL_1:74;
hence (p2 `2 ) / (p2 `1 ) <= 1 by A76, XCMPLX_1:60; :: thesis: verum

end;

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

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

end;

end;

end;

A90: now

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

case A91: ( 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 A91, XREAL_1:74;
hence (p1 `1 ) / (p1 `2 ) <= 1 by A78, XCMPLX_1:60; :: thesis: verum

end;

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

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

end;

end;

end;

A94: now

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

case A95: ( 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 A95, XREAL_1:74;
hence - 1 <= (p2 `2 ) / (p2 `1 ) by A76, XCMPLX_1:198; :: thesis: verum

end;

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

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

end;

end;

end;

A99: now

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

case A100: ( 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 A100, XREAL_1:74;
hence - 1 <= (p1 `1 ) / (p1 `2 ) by A78, XCMPLX_1:198; :: thesis: verum

end;

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

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

end;

end;

end;

now

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

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

then B105: ( ( p1 `1 > 0 & p1 `2 >= 0 ) or ( p1 `1 < 0 & p1 `2 <= 0 ) ) by A83, A81;

now

assume (p1 `1 ) / (p1 `2 ) <> 1 ; :: thesis: contradiction
then (p1 `1 ) / (p1 `2 ) < 1 by A90, XXREAL_0:1;
hence contradiction by A81, A86, A104, B105, XREAL_1:164; :: thesis: verum

end;

then p1 `1 = 1 * (p1 `2 ) by A78, XCMPLX_1:88;
then ((p2 `2 ) / (p2 `1 )) * (p2 `1 ) = 1 * (p2 `1 ) by A78, A84, XCMPLX_1:60
.= p2 `1 ;
then p2 `2 = p2 `1 by A76, XCMPLX_1:88;
hence contradiction by A73, A85; :: thesis: verum

end;

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

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

now

assume (p1 `1 ) / (p1 `2 ) <> - 1 ; :: thesis: contradiction
then - 1 < (p1 `1 ) / (p1 `2 ) by A99, XXREAL_0:1;
hence contradiction by A81, A94, A106, B107, XREAL_1:168; :: thesis: verum

end;

then p1 `1 = (- 1) * (p1 `2 ) by A78, XCMPLX_1:88
.= - (p1 `2 ) ;
then - (p1 `1 ) = p1 `2 ;
then (p2 `2 ) / (p2 `1 ) = - 1 by A83, A84, XCMPLX_1:198;
then p2 `2 = (- 1) * (p2 `1 ) by A76, XCMPLX_1:88;
then - (p2 `2 ) = p2 `1 ;
hence contradiction by A73, A85; :: 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 A108: Out_In_Sq is one-to-one by FUNCT_1:def 8;
A109: 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 A110: ( t in K0 & t <> 0. (TOP-REAL 2) ) ; :: thesis: not Out_In_Sq . t in K0 \/ Kb
then consider p3 being Point of (TOP-REAL 2) such that
A111: ( p3 = t & - 1 < p3 `1 & p3 `1 < 1 & - 1 < p3 `2 & p3 `2 < 1 ) by A1;

now

assume A112: 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 A112, XBOOLE_0:def 3;

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

then consider p4 being Point of (TOP-REAL 2) such that
A113: ( p4 = Out_In_Sq . t & - 1 < p4 `1 & p4 `1 < 1 & - 1 < p4 `2 & 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 A114: ( ( 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 A110, Def1;
then A115: ( p4 `1 = 1 / (t `1 ) & p4 `2 = ((t `2 ) / (t `1 )) / (t `1 ) ) by A113, EUCLID:56;

now

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

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

now

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

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

then (1 / (t `1 )) * (t `1 ) < 1 * (t `1 ) by A113, A115, XREAL_1:70;
hence contradiction by A111, A117, XCMPLX_1:88; :: thesis: verum

end;

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

then t `2 = 0 by A114;
hence contradiction by A110, A118, EUCLID:57, EUCLID:58; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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

then (- 1) * (t `1 ) > (1 / (t `1 )) * (t `1 ) by A113, A115, XREAL_1:71;
then (- 1) * (t `1 ) > 1 by A119, XCMPLX_1:88;
then - (- (t `1 )) <= - 1 by XREAL_1:26;
hence contradiction by A111; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

case A120: ( 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 A110, Def1;
then A121: ( p4 `2 = 1 / (t `2 ) & p4 `1 = ((t `1 ) / (t `2 )) / (t `2 ) ) by A113, EUCLID:56;

now

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

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

now

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

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

then (1 / (t `2 )) * (t `2 ) < 1 * (t `2 ) by A113, A121, XREAL_1:70;
hence contradiction by A111, A125, XCMPLX_1:88; :: thesis: verum

end;

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

hence contradiction by A120; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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

then (- 1) * (t `2 ) > (1 / (t `2 )) * (t `2 ) by A113, A121, XREAL_1:71;
then (- 1) * (t `2 ) > 1 by A126, XCMPLX_1:88;
then - (- (t `2 )) <= - 1 by XREAL_1:26;
hence contradiction by A111; :: 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
A127: ( p4 = Out_In_Sq . 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;

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

then A129: Out_In_Sq . t = |[(1 / (t `1 )),(((t `2 ) / (t `1 )) / (t `1 ))]| by A110, Def1;
then A130: ( p4 `1 = 1 / (t `1 ) & p4 `2 = ((t `2 ) / (t `1 )) / (t `1 ) ) by A127, 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 A127;

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

then 1 * ((t `1 ) " ) = - 1 by A130;
then A131: (t `1 ) * ((t `1 ) " ) = - (t `1 ) ;

now

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

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

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

end;

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

then t `2 = 0 by A128;
hence contradiction by A110, A132, 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 1 * ((t `1 ) " ) = 1 by A130;
then A133: (t `1 ) * ((t `1 ) " ) = t `1 ;

now

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

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

hence contradiction by A111, A133, XCMPLX_0:def 7; :: thesis: verum

end;

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

then t `2 = 0 by A128;
hence contradiction by A110, A134, EUCLID:57, EUCLID:58; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

case A135: ( - 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 A3, Th27;
A136: rng (Out_In_Sq | K01) c= the carrier of (((TOP-REAL 2) | D) | K01) by Th25;
A137: dom (Out_In_Sq | K01) = (dom Out_In_Sq ) /\ K01 by RELAT_1:90
.= D /\ K01 by A2, 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 A110, A128;
then (Out_In_Sq | K01) . t in rng (Out_In_Sq | K01) by A137, FUNCT_1:12;
then A138: (Out_In_Sq | K01) . t in the carrier of (((TOP-REAL 2) | D) | K01) by A136;
A139: the carrier of (((TOP-REAL 2) | D) | K01) = [#] (((TOP-REAL 2) | D) | K01)
.= K01 by PRE_TOPC:def 10 ;
t in K01 by A110, A128;
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 A138, A139, FUNCT_1:72;
then consider p5 being Point of (TOP-REAL 2) such that
A140: ( 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 A127;

now

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

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

then A141: 1 / (t `1 ) = 1 by A130, A135, XXREAL_0:1;
then ((t `2 ) / (t `1 )) / (t `1 ) = ((t `2 ) / (t `1 )) * 1
.= (t `2 ) * 1 by A141
.= t `2 ;
hence contradiction by A111, A127, A129, A135, EUCLID:56; :: thesis: verum

end;

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

then A142: 1 / (t `1 ) = - 1 by A130, A135, XXREAL_0:1;
then ((t `2 ) / (t `1 )) / (t `1 ) = ((t `2 ) / (t `1 )) * (- 1)
.= - ((t `2 ) / (t `1 ))
.= - ((t `2 ) * (- 1)) by A142
.= t `2 ;
hence contradiction by A111, A127, A129, A135, EUCLID:56; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

case A143: ( 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 A3, Th27;
A144: rng (Out_In_Sq | K01) c= the carrier of (((TOP-REAL 2) | D) | K01) by Th25;
dom (Out_In_Sq | K01) = (dom Out_In_Sq ) /\ K01 by RELAT_1:90
.= D /\ K01 by A2, 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 A110, A128;
then (Out_In_Sq | K01) . t in rng (Out_In_Sq | K01) by FUNCT_1:12;
then A145: (Out_In_Sq | K01) . t in the carrier of (((TOP-REAL 2) | D) | K01) by A144;
A146: the carrier of (((TOP-REAL 2) | D) | K01) = [#] (((TOP-REAL 2) | D) | K01)
.= K01 by PRE_TOPC:def 10 ;
t in K01 by A110, A128;
then Out_In_Sq . t = (Out_In_Sq | K01) . t by FUNCT_1:72;
then consider p5 being Point of (TOP-REAL 2) such that
A147: ( 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 A127, A145, A146;

now

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

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

then A148: 1 / (t `1 ) = 1 by A130, A143, XXREAL_0:1;
then ((t `2 ) / (t `1 )) / (t `1 ) = ((t `2 ) / (t `1 )) * 1
.= (t `2 ) * 1 by A148
.= t `2 ;
hence contradiction by A111, A127, A129, A143, EUCLID:56; :: thesis: verum

end;

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

then A149: 1 / (t `1 ) = - 1 by A130, A143, XXREAL_0:1;
then ((t `2 ) / (t `1 )) / (t `1 ) = ((t `2 ) / (t `1 )) * (- 1)
.= - ((t `2 ) / (t `1 ))
.= - ((t `2 ) * (- 1)) by A149
.= t `2 ;
hence contradiction by A111, A127, A129, A143, EUCLID:56; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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

then A151: Out_In_Sq . t = |[(((t `1 ) / (t `2 )) / (t `2 )),(1 / (t `2 ))]| by A110, Def1;
then A152: ( p4 `2 = 1 / (t `2 ) & p4 `1 = ((t `1 ) / (t `2 )) / (t `2 ) ) by A127, 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 A127;

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

then 1 * ((t `2 ) " ) = - 1 by A152;
then A155: (t `2 ) * ((t `2 ) " ) = - (t `2 ) ;

now

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

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

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

end;

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

hence contradiction by A150; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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

then 1 * ((t `2 ) " ) = 1 by A152;
then A156: (t `2 ) * ((t `2 ) " ) = t `2 ;

now

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

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

hence contradiction by A111, A156, XCMPLX_0:def 7; :: thesis: verum

end;

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

hence contradiction by A150; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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

A158: ( ( t `1 <= t `2 & - (t `2 ) <= t `1 ) or ( t `1 >= t `2 & t `1 <= - (t `2 ) ) ) by A150, Th23;
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 A3, Th28;
A159: rng (Out_In_Sq | K11) c= the carrier of (((TOP-REAL 2) | D) | K11) by Th26;
A160: dom (Out_In_Sq | K11) = (dom Out_In_Sq ) /\ K11 by RELAT_1:90
.= D /\ K11 by A2, 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 ;
t in K11 by A110, A158;
then (Out_In_Sq | K11) . t in rng (Out_In_Sq | K11) by A160, FUNCT_1:12;
then A161: (Out_In_Sq | K11) . t in the carrier of (((TOP-REAL 2) | D) | K11) by A159;
A162: the carrier of (((TOP-REAL 2) | D) | K11) = [#] (((TOP-REAL 2) | D) | K11)
.= K11 by PRE_TOPC:def 10 ;
t in K11 by A110, A158;
then Out_In_Sq . t = (Out_In_Sq | K11) . t by FUNCT_1:72;
then consider p5 being Point of (TOP-REAL 2) such that
A163: ( 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 A127, A161, A162;

now

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

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

then A164: 1 / (t `2 ) = 1 by A152, A157, XXREAL_0:1;
then ((t `1 ) / (t `2 )) / (t `2 ) = ((t `1 ) / (t `2 )) * 1
.= (t `1 ) * 1 by A164
.= t `1 ;
hence contradiction by A111, A127, A151, A157, EUCLID:56; :: thesis: verum

end;

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

then A165: 1 / (t `2 ) = - 1 by A152, A157, XXREAL_0:1;
then ((t `1 ) / (t `2 )) / (t `2 ) = ((t `1 ) / (t `2 )) * (- 1)
.= - ((t `1 ) / (t `2 ))
.= - ((t `1 ) * (- 1)) by A165
.= t `1 ;
hence contradiction by A111, A127, A151, A157, EUCLID:56; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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

A167: ( ( t `1 <= t `2 & - (t `2 ) <= t `1 ) or ( t `1 >= t `2 & t `1 <= - (t `2 ) ) ) by A150, Th23;
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 A3, Th28;
A168: rng (Out_In_Sq | K11) c= the carrier of (((TOP-REAL 2) | D) | K11) by Th26;
A169: dom (Out_In_Sq | K11) = (dom Out_In_Sq ) /\ K11 by RELAT_1:90
.= D /\ K11 by A2, 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 ;
t in K11 by A110, A167;
then (Out_In_Sq | K11) . t in rng (Out_In_Sq | K11) by A169, FUNCT_1:12;
then A170: (Out_In_Sq | K11) . t in the carrier of (((TOP-REAL 2) | D) | K11) by A168;
A171: the carrier of (((TOP-REAL 2) | D) | K11) = [#] (((TOP-REAL 2) | D) | K11)
.= K11 by PRE_TOPC:def 10 ;
t in K11 by A110, A167;
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 A170, A171, FUNCT_1:72;
then consider p5 being Point of (TOP-REAL 2) such that
A172: ( 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 A127;

now

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

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

then A173: 1 / (t `2 ) = 1 by A152, A166, XXREAL_0:1;
then ((t `1 ) / (t `2 )) / (t `2 ) = ((t `1 ) / (t `2 )) * 1
.= (t `1 ) * 1 by A173
.= t `1 ;
hence contradiction by A111, A127, A151, A166, EUCLID:56; :: thesis: verum

end;

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

then A174: 1 / (t `2 ) = - 1 by A152, A166, XXREAL_0:1;
then ((t `1 ) / (t `2 )) / (t `2 ) = ((t `1 ) / (t `2 )) * (- 1)
.= - ((t `1 ) / (t `2 ))
.= - ((t `1 ) * (- 1)) by A174
.= t `1 ;
hence contradiction by A111, A127, A151, A166, 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;

A175: 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 not t in K0 \/ Kb ; :: thesis: Out_In_Sq . t in K0
then A176: ( not t in K0 & not t in Kb ) by XBOOLE_0:def 3;
then A177: 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) ;

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

then Out_In_Sq . t = |[(1 / (t `1 )),(((t `2 ) / (t `1 )) / (t `1 ))]| by A177, Def1;
then A179: ( p4 `1 = 1 / (t `1 ) & p4 `2 = ((t `2 ) / (t `1 )) / (t `1 ) ) by EUCLID:56;

now

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

case A180: 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 A182: 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, A176;
then A184: t `1 >= 1 by A178, A182, A180, XXREAL_0:2;
not t `1 = 1 by A1, A176, A178;
then A185: t `1 > 1 by A184, XXREAL_0:1;
then A186: (t `1 ) / (t `1 ) > 1 / (t `1 ) by XREAL_1:76;
A187: 0 < (t `2 ) / (t `1 ) by A180, A182, XREAL_1:141;
A188: ((- 1) * (t `1 )) / (t `1 ) < ((t `2 ) / (t `1 )) / (t `1 ) by A180, A187, XREAL_1:76;
t `1 < (t `1 ) ^2 by A185, SQUARE_1:76;
then t `2 < (t `1 ) ^2 by A178, A180, XXREAL_0:2;
then (t `2 ) / (t `1 ) < ((t `1 ) ^2 ) / (t `1 ) by A180, XREAL_1:76;
then (t `2 ) / (t `1 ) < t `1 by A180, XCMPLX_1:90;
then ((t `2 ) / (t `1 )) / (t `1 ) < (t `1 ) / (t `1 ) by A180, 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 A180, A186, A188, XCMPLX_1:60, XCMPLX_1:90; :: thesis: verum

end;

case A189: 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 )

A190: - (- (t `1 )) >= - (t `2 ) by A178, A180, XREAL_1:26;

A191: now

assume t `1 < 1 ; :: thesis: t `1 >= 1
then - 1 >= t `2 by A1, A176, A180, A189;
then - (t `1 ) <= - 1 by A178, A180, XXREAL_0:2;
hence t `1 >= 1 by XREAL_1:26; :: thesis: verum

end;

not t `1 = 1 by A1, A176, A178;
then A192: t `1 > 1 by A191, XXREAL_0:1;
then A193: (t `1 ) / (t `1 ) > 1 / (t `1 ) by XREAL_1:76;
t `1 < (t `1 ) ^2 by A192, SQUARE_1:76;
then (t `1 ) ^2 > - (t `2 ) by A190, XXREAL_0:2;
then ((t `1 ) ^2 ) / (t `1 ) > (- (t `2 )) / (t `1 ) by A180, XREAL_1:76;
then t `1 > (- (t `2 )) / (t `1 ) by A180, XCMPLX_1:90;
then t `1 > - ((t `2 ) / (t `1 )) ;
then - (t `1 ) < - (- ((t `2 ) / (t `1 ))) by XREAL_1:26;
then ((- 1) * (t `1 )) / (t `1 ) < ((t `2 ) / (t `1 )) / (t `1 ) by A180, 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 A193, A180, A189, 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 A195: 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 A195;

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

then t `2 = 0 by A178;
hence contradiction by A1, A176, A196; :: thesis: verum

end;

case A197: 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 A199: 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, A176;
then ( t `1 <= - 1 or 1 <= - (t `1 ) ) by A178, A197, XXREAL_0:2;
then A200: ( t `1 <= - 1 or - 1 >= - (- (t `1 )) ) by XREAL_1:26;
not t `1 = - 1 by A1, A176, A178;
then A201: t `1 < - 1 by A200, XXREAL_0:1;
then (t `1 ) / (t `1 ) > (- 1) / (t `1 ) by XREAL_1:77;
then - ((t `1 ) / (t `1 )) < - ((- 1) / (t `1 )) by XREAL_1:26;
then A202: - ((t `1 ) / (t `1 )) < 1 / (t `1 ) ;
A203: 0 > (t `2 ) / (t `1 ) by A197, A199, XREAL_1:144;
A204: ((- 1) * (t `1 )) / (t `1 ) < ((t `2 ) / (t `1 )) / (t `1 ) by A197, A203, XREAL_1:77;
- (t `1 ) < (t `1 ) ^2 by A201, SQUARE_1:116;
then t `2 < (t `1 ) ^2 by A178, A197, XXREAL_0:2;
then (t `2 ) / (t `1 ) > ((t `1 ) ^2 ) / (t `1 ) by A197, XREAL_1:77;
then (t `2 ) / (t `1 ) > t `1 by A197, XCMPLX_1:90;
then ((t `2 ) / (t `1 )) / (t `1 ) < (t `1 ) / (t `1 ) by A197, 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 A197, A202, A204, XCMPLX_1:60; :: thesis: verum

end;

case A205: 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, A176, A197;
then A206: t `1 <= - 1 by A178, A197, XXREAL_0:2;
not t `1 = - 1 by A1, A176, A178;
then A207: t `1 < - 1 by A206, XXREAL_0:1;
then (t `1 ) / (t `1 ) > (- 1) / (t `1 ) by XREAL_1:77;
then 1 > (- 1) / (t `1 ) by A197, XCMPLX_1:60;
then A208: - 1 < - ((- 1) / (t `1 )) by XREAL_1:26;
A209: - (t `1 ) >= - (t `2 ) by A178, A197, XREAL_1:26;
- (t `1 ) < (t `1 ) ^2 by A207, SQUARE_1:116;
then (t `1 ) ^2 > - (t `2 ) by A209, XXREAL_0:2;
then ((t `1 ) ^2 ) / (t `1 ) < (- (t `2 )) / (t `1 ) by A197, XREAL_1:77;
then t `1 < (- (t `2 )) / (t `1 ) by A197, XCMPLX_1:90;
then t `1 < - ((t `2 ) / (t `1 )) ;
then - (t `1 ) > - (- ((t `2 ) / (t `1 ))) by XREAL_1:26;
then A210: ((- 1) * (t `1 )) / (t `1 ) < ((t `2 ) / (t `1 )) / (t `1 ) by A197, XREAL_1:77;
((t `2 ) / (t `1 )) / (t `1 ) < (t `1 ) / (t `1 ) by A197, A205, 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 A197, A208, A210, 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;

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 Out_In_Sq . t in K0 by A1, A179; :: thesis: verum

end;

case A211: ( 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 Out_In_Sq . t = |[(((t `1 ) / (t `2 )) / (t `2 )),(1 / (t `2 ))]| by A177, Def1;
then A212: ( p4 `2 = 1 / (t `2 ) & p4 `1 = ((t `1 ) / (t `2 )) / (t `2 ) ) by EUCLID:56;
A213: ( ( t `1 <= t `2 & - (t `2 ) <= t `1 ) or ( t `1 >= t `2 & t `1 <= - (t `2 ) ) ) by A211, Th23;

now

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

case A214: 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 A216: 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 )

A218: ( - 1 >= t `2 or t `2 >= 1 or - 1 >= t `1 or t `1 >= 1 ) by A1, A176;
not t `2 = 1 by A1, A176, A211, A216;
then A219: t `2 > 1 by A211, A216, A214, A218, XXREAL_0:1, XXREAL_0:2;
then A220: (t `2 ) / (t `2 ) > 1 / (t `2 ) by XREAL_1:76;
A221: 0 < (t `1 ) / (t `2 ) by A214, A216, XREAL_1:141;
A222: ((- 1) * (t `2 )) / (t `2 ) < ((t `1 ) / (t `2 )) / (t `2 ) by A214, A221, XREAL_1:76;
t `2 < (t `2 ) ^2 by A219, SQUARE_1:76;
then t `1 < (t `2 ) ^2 by A211, A214, XXREAL_0:2;
then (t `1 ) / (t `2 ) < ((t `2 ) ^2 ) / (t `2 ) by A214, XREAL_1:76;
then (t `1 ) / (t `2 ) < t `2 by A214, XCMPLX_1:90;
then ((t `1 ) / (t `2 )) / (t `2 ) < (t `2 ) / (t `2 ) by A214, 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 A214, A220, A222, XCMPLX_1:60, XCMPLX_1:90; :: thesis: verum

end;

case A223: 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 )

A224: now

assume t `2 < 1 ; :: thesis: t `2 >= 1
then - 1 >= t `1 by A1, A176, A214, A223;
then - (t `2 ) <= - 1 by A213, A214, XXREAL_0:2;
hence t `2 >= 1 by XREAL_1:26; :: thesis: verum

end;

not t `2 = 1 by A1, A176, A213;
then A225: t `2 > 1 by A224, XXREAL_0:1;
then A226: (t `2 ) / (t `2 ) > 1 / (t `2 ) by XREAL_1:76;
t `2 < (t `2 ) ^2 by A225, SQUARE_1:76;
then (t `2 ) ^2 > - (t `1 ) by A211, A214, XXREAL_0:2;
then ((t `2 ) ^2 ) / (t `2 ) > (- (t `1 )) / (t `2 ) by A214, XREAL_1:76;
then t `2 > (- (t `1 )) / (t `2 ) by A214, XCMPLX_1:90;
then t `2 > - ((t `1 ) / (t `2 )) ;
then - (t `2 ) < - (- ((t `1 ) / (t `2 ))) by XREAL_1:26;
then A227: ((- 1) * (t `2 )) / (t `2 ) < ((t `1 ) / (t `2 )) / (t `2 ) by A214, XREAL_1:76;
((t `1 ) / (t `2 )) / (t `2 ) < (t `2 ) / (t `2 ) by A214, A223, 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 A214, A226, A227, 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 A228: 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 )

X: t `2 <> 0 by A211;

now

A230: t `2 < 0 by A228, X;
A232: ( t `1 <= t `2 or t `1 <= - (t `2 ) ) by A211, Th23;

now

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

case A233: 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, A176;
then ( t `2 <= - 1 or 1 <= - (t `2 ) ) by A213, A230, XXREAL_0:2;
then A234: ( t `2 <= - 1 or - 1 >= - (- (t `2 )) ) by XREAL_1:26;
not t `2 = - 1 by A1, A176, A213;
then A235: t `2 < - 1 by A234, XXREAL_0:1;
then (t `2 ) / (t `2 ) > (- 1) / (t `2 ) by XREAL_1:77;
then - ((t `2 ) / (t `2 )) < - ((- 1) / (t `2 )) by XREAL_1:26;
then A236: - ((t `2 ) / (t `2 )) < 1 / (t `2 ) ;
A237: 0 > (t `1 ) / (t `2 ) by A230, A233, XREAL_1:144;
A238: ((- 1) * (t `2 )) / (t `2 ) < ((t `1 ) / (t `2 )) / (t `2 ) by A230, A237, XREAL_1:77;
- (t `2 ) < (t `2 ) ^2 by A235, SQUARE_1:116;
then t `1 < (t `2 ) ^2 by A230, A232, XXREAL_0:2;
then (t `1 ) / (t `2 ) > ((t `2 ) ^2 ) / (t `2 ) by A230, XREAL_1:77;
then (t `1 ) / (t `2 ) > t `2 by A230, XCMPLX_1:90;
then ((t `1 ) / (t `2 )) / (t `2 ) < (t `2 ) / (t `2 ) by A230, 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 A230, A236, A238, XCMPLX_1:60; :: thesis: verum

end;

case A239: 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 )

then A240: ( - 1 >= t `2 or - 1 >= t `1 ) by A1, A176, A230;
not t `2 = - 1 by A1, A176, A213;
then A241: t `2 < - 1 by A211, A230, A240, XXREAL_0:1, XXREAL_0:2;
then (t `2 ) / (t `2 ) > (- 1) / (t `2 ) by XREAL_1:77;
then 1 > (- 1) / (t `2 ) by A230, XCMPLX_1:60;
then A242: - 1 < - ((- 1) / (t `2 )) by XREAL_1:26;
A243: - (t `2 ) >= - (t `1 ) by A211, A230, XREAL_1:26;
- (t `2 ) < (t `2 ) ^2 by A241, SQUARE_1:116;
then (t `2 ) ^2 > - (t `1 ) by A243, XXREAL_0:2;
then ((t `2 ) ^2 ) / (t `2 ) < (- (t `1 )) / (t `2 ) by A230, XREAL_1:77;
then t `2 < (- (t `1 )) / (t `2 ) by A230, XCMPLX_1:90;
then t `2 < - ((t `1 ) / (t `2 )) ;
then - (t `2 ) > - (- ((t `1 ) / (t `2 ))) by XREAL_1:26;
then ((- 1) * (t `2 )) / (t `2 ) < ((t `1 ) / (t `2 )) / (t `2 ) by A230, 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 A242, A230, A239, 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;

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;

hence Out_In_Sq . t in K0 by A1, A212; :: thesis: verum

end;

end;

end;

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

end;

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 consider p4 being Point of (TOP-REAL 2) such that
A245: ( 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;
A246: not t = 0. (TOP-REAL 2) by A245, EUCLID:56, EUCLID:58;
A247: t <> 0. (TOP-REAL 2) by A245, 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 A248: ( ( t `2 <= t `1 & - (t `1 ) <= t `2 ) or ( t `2 >= t `1 & t `2 <= - (t `1 ) ) ) ; :: thesis: Out_In_Sq . t = t

then A249: Out_In_Sq . t = |[(1 / (t `1 )),(((t `2 ) / (t `1 )) / (t `1 ))]| by A246, Def1;
A250: ( ( 1 <= t `1 & t `1 >= - 1 ) or ( 1 >= t `1 & - 1 >= - (- (t `1 )) ) ) by A245, A248, XREAL_1:26;

now

per cases ( t `1 = 1 or t `1 = - 1 ) by A245, A250, XXREAL_0:1;

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

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

end;

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

thus Out_In_Sq . t = t by A249, A251, EUCLID:57; :: thesis: verum

end;

end;

end;

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

end;

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

now

per cases ( t `2 = 1 or t `2 = - 1 ) by A245, A252;

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

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

end;

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

thus Out_In_Sq . t = t by A253, A254, 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;

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 A4, A108, A109, A175; :: thesis: verum