let K0, C0 be Subset of (TOP-REAL 2); :: thesis: ( K0 = { p where p is Point of (TOP-REAL 2) : ( - 1 <= p `1 & p `1 <= 1 & - 1 <= p `2 & p `2 <= 1 ) } & C0 = { p1 where p1 is Point of (TOP-REAL 2) : |.p1.| <= 1 } implies Sq_Circ " C0 c= K0 )
assume A1: ( K0 = { p where p is Point of (TOP-REAL 2) : ( - 1 <= p `1 & p `1 <= 1 & - 1 <= p `2 & p `2 <= 1 ) } & C0 = { p1 where p1 is Point of (TOP-REAL 2) : |.p1.| <= 1 } ) ; :: thesis: Sq_Circ " C0 c= K0
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Sq_Circ " C0 or x in K0 )
assume A2: x in Sq_Circ " C0 ; :: thesis: x in K0
then reconsider px = x as Point of (TOP-REAL 2) ;
set q = px;
A3: Sq_Circ . x in C0 by A2, FUNCT_1:def 7;
now :: thesis: ( ( px = 0. (TOP-REAL 2) & - 1 <= px `1 & px `1 <= 1 & - 1 <= px `2 & px `2 <= 1 ) or ( px <> 0. (TOP-REAL 2) & ( ( px `2 <= px `1 & - (px `1) <= px `2 ) or ( px `2 >= px `1 & px `2 <= - (px `1) ) ) & - 1 <= px `1 & px `1 <= 1 & - 1 <= px `2 & px `2 <= 1 ) or ( px <> 0. (TOP-REAL 2) & not ( px `2 <= px `1 & - (px `1) <= px `2 ) & not ( px `2 >= px `1 & px `2 <= - (px `1) ) & - 1 <= px `1 & px `1 <= 1 & - 1 <= px `2 & px `2 <= 1 ) )
per cases ( px = 0. (TOP-REAL 2) or ( px <> 0. (TOP-REAL 2) & ( ( px `2 <= px `1 & - (px `1) <= px `2 ) or ( px `2 >= px `1 & px `2 <= - (px `1) ) ) ) or ( px <> 0. (TOP-REAL 2) & not ( px `2 <= px `1 & - (px `1) <= px `2 ) & not ( px `2 >= px `1 & px `2 <= - (px `1) ) ) ) ;
case px = 0. (TOP-REAL 2) ; :: thesis: ( - 1 <= px `1 & px `1 <= 1 & - 1 <= px `2 & px `2 <= 1 )
hence ( - 1 <= px `1 & px `1 <= 1 & - 1 <= px `2 & px `2 <= 1 ) by JGRAPH_2:3; :: thesis: verum
end;
case A4: ( px <> 0. (TOP-REAL 2) & ( ( px `2 <= px `1 & - (px `1) <= px `2 ) or ( px `2 >= px `1 & px `2 <= - (px `1) ) ) ) ; :: thesis: ( - 1 <= px `1 & px `1 <= 1 & - 1 <= px `2 & px `2 <= 1 )
A5: now :: thesis: not ((px `1) ^2) + ((px `2) ^2) = 0
assume ((px `1) ^2) + ((px `2) ^2) = 0 ; :: thesis: contradiction
then ( px `1 = 0 & px `2 = 0 ) by COMPLEX1:1;
hence contradiction by A4, EUCLID:53, EUCLID:54; :: thesis: verum
end;
A6: (px `1) ^2 >= 0 by XREAL_1:63;
A9: ( |[((px `1) / (sqrt (1 + (((px `2) / (px `1)) ^2)))),((px `2) / (sqrt (1 + (((px `2) / (px `1)) ^2))))]| `1 = (px `1) / (sqrt (1 + (((px `2) / (px `1)) ^2))) & |[((px `1) / (sqrt (1 + (((px `2) / (px `1)) ^2)))),((px `2) / (sqrt (1 + (((px `2) / (px `1)) ^2))))]| `2 = (px `2) / (sqrt (1 + (((px `2) / (px `1)) ^2))) ) by EUCLID:52;
consider p1 being Point of (TOP-REAL 2) such that
A10: p1 = Sq_Circ . px and
A11: |.p1.| <= 1 by A1, A3;
|.p1.| ^2 <= |.p1.| by A11, SQUARE_1:42;
then A12: |.p1.| ^2 <= 1 by A11, XXREAL_0:2;
A13: 1 + (((px `2) / (px `1)) ^2) > 0 by Lm1;
Sq_Circ . px = |[((px `1) / (sqrt (1 + (((px `2) / (px `1)) ^2)))),((px `2) / (sqrt (1 + (((px `2) / (px `1)) ^2))))]| by A4, Def1;
then |.p1.| ^2 = (((px `1) / (sqrt (1 + (((px `2) / (px `1)) ^2)))) ^2) + (((px `2) / (sqrt (1 + (((px `2) / (px `1)) ^2)))) ^2) by A9, A10, JGRAPH_1:29
.= (((px `1) ^2) / ((sqrt (1 + (((px `2) / (px `1)) ^2))) ^2)) + (((px `2) / (sqrt (1 + (((px `2) / (px `1)) ^2)))) ^2) by XCMPLX_1:76
.= (((px `1) ^2) / ((sqrt (1 + (((px `2) / (px `1)) ^2))) ^2)) + (((px `2) ^2) / ((sqrt (1 + (((px `2) / (px `1)) ^2))) ^2)) by XCMPLX_1:76
.= (((px `1) ^2) / (1 + (((px `2) / (px `1)) ^2))) + (((px `2) ^2) / ((sqrt (1 + (((px `2) / (px `1)) ^2))) ^2)) by A13, SQUARE_1:def 2
.= (((px `1) ^2) / (1 + (((px `2) / (px `1)) ^2))) + (((px `2) ^2) / (1 + (((px `2) / (px `1)) ^2))) by A13, SQUARE_1:def 2
.= (((px `1) ^2) + ((px `2) ^2)) / (1 + (((px `2) / (px `1)) ^2)) by XCMPLX_1:62 ;
then ((((px `1) ^2) + ((px `2) ^2)) / (1 + (((px `2) / (px `1)) ^2))) * (1 + (((px `2) / (px `1)) ^2)) <= 1 * (1 + (((px `2) / (px `1)) ^2)) by A13, A12, XREAL_1:64;
then ((px `1) ^2) + ((px `2) ^2) <= 1 + (((px `2) / (px `1)) ^2) by A13, XCMPLX_1:87;
then ((px `1) ^2) + ((px `2) ^2) <= 1 + (((px `2) ^2) / ((px `1) ^2)) by XCMPLX_1:76;
then (((px `1) ^2) + ((px `2) ^2)) - 1 <= (1 + (((px `2) ^2) / ((px `1) ^2))) - 1 by XREAL_1:9;
then ((((px `1) ^2) + ((px `2) ^2)) - 1) * ((px `1) ^2) <= (((px `2) ^2) / ((px `1) ^2)) * ((px `1) ^2) by A6, XREAL_1:64;
then (((px `1) ^2) * ((px `1) ^2)) + ((((px `2) ^2) - 1) * ((px `1) ^2)) <= (px `2) ^2 by A7, XCMPLX_1:6, XCMPLX_1:87;
then (((((px `1) ^2) * ((px `1) ^2)) - (((px `1) ^2) * 1)) + (((px `1) ^2) * ((px `2) ^2))) - (1 * ((px `2) ^2)) <= 0 by XREAL_1:47;
then A14: (((px `1) ^2) - 1) * (((px `1) ^2) + ((px `2) ^2)) <= 0 ;
(px `2) ^2 >= 0 by XREAL_1:63;
then A15: ((px `1) ^2) - 1 <= 0 by A6, A14, A5, XREAL_1:129;
then A16: px `1 <= 1 by SQUARE_1:43;
A17: - 1 <= px `1 by A15, SQUARE_1:43;
then ( ( px `2 <= 1 & - (- (px `1)) >= - (px `2) ) or ( px `2 >= - 1 & - (px `2) >= - (- (px `1)) ) ) by A4, A16, XREAL_1:24, XXREAL_0:2;
then ( ( px `2 <= 1 & 1 >= - (px `2) ) or ( px `2 >= - 1 & - (px `2) >= px `1 ) ) by A16, XXREAL_0:2;
then ( ( px `2 <= 1 & - 1 <= - (- (px `2)) ) or ( px `2 >= - 1 & - (px `2) >= - 1 ) ) by A17, XREAL_1:24, XXREAL_0:2;
hence ( - 1 <= px `1 & px `1 <= 1 & - 1 <= px `2 & px `2 <= 1 ) by A15, SQUARE_1:43, XREAL_1:24; :: thesis: verum
end;
case A18: ( px <> 0. (TOP-REAL 2) & not ( px `2 <= px `1 & - (px `1) <= px `2 ) & not ( px `2 >= px `1 & px `2 <= - (px `1) ) ) ; :: thesis: ( - 1 <= px `1 & px `1 <= 1 & - 1 <= px `2 & px `2 <= 1 )
A19: now :: thesis: not ((px `2) ^2) + ((px `1) ^2) = 0
assume ((px `2) ^2) + ((px `1) ^2) = 0 ; :: thesis: contradiction
then px `2 = 0 by COMPLEX1:1;
hence contradiction by A18; :: thesis: verum
end;
A20: (px `2) ^2 >= 0 by XREAL_1:63;
A21: px `2 <> 0 by A18;
A22: ( |[((px `1) / (sqrt (1 + (((px `1) / (px `2)) ^2)))),((px `2) / (sqrt (1 + (((px `1) / (px `2)) ^2))))]| `2 = (px `2) / (sqrt (1 + (((px `1) / (px `2)) ^2))) & |[((px `1) / (sqrt (1 + (((px `1) / (px `2)) ^2)))),((px `2) / (sqrt (1 + (((px `1) / (px `2)) ^2))))]| `1 = (px `1) / (sqrt (1 + (((px `1) / (px `2)) ^2))) ) by EUCLID:52;
consider p1 being Point of (TOP-REAL 2) such that
A23: p1 = Sq_Circ . px and
A24: |.p1.| <= 1 by A1, A3;
|.p1.| ^2 <= |.p1.| by A24, SQUARE_1:42;
then A25: |.p1.| ^2 <= 1 by A24, XXREAL_0:2;
A26: 1 + (((px `1) / (px `2)) ^2) > 0 by Lm1;
Sq_Circ . px = |[((px `1) / (sqrt (1 + (((px `1) / (px `2)) ^2)))),((px `2) / (sqrt (1 + (((px `1) / (px `2)) ^2))))]| by A18, Def1;
then |.p1.| ^2 = (((px `1) / (sqrt (1 + (((px `1) / (px `2)) ^2)))) ^2) + (((px `2) / (sqrt (1 + (((px `1) / (px `2)) ^2)))) ^2) by A22, A23, JGRAPH_1:29
.= (((px `2) ^2) / ((sqrt (1 + (((px `1) / (px `2)) ^2))) ^2)) + (((px `1) / (sqrt (1 + (((px `1) / (px `2)) ^2)))) ^2) by XCMPLX_1:76
.= (((px `2) ^2) / ((sqrt (1 + (((px `1) / (px `2)) ^2))) ^2)) + (((px `1) ^2) / ((sqrt (1 + (((px `1) / (px `2)) ^2))) ^2)) by XCMPLX_1:76
.= (((px `2) ^2) / (1 + (((px `1) / (px `2)) ^2))) + (((px `1) ^2) / ((sqrt (1 + (((px `1) / (px `2)) ^2))) ^2)) by A26, SQUARE_1:def 2
.= (((px `2) ^2) / (1 + (((px `1) / (px `2)) ^2))) + (((px `1) ^2) / (1 + (((px `1) / (px `2)) ^2))) by A26, SQUARE_1:def 2
.= (((px `2) ^2) + ((px `1) ^2)) / (1 + (((px `1) / (px `2)) ^2)) by XCMPLX_1:62 ;
then ((((px `2) ^2) + ((px `1) ^2)) / (1 + (((px `1) / (px `2)) ^2))) * (1 + (((px `1) / (px `2)) ^2)) <= 1 * (1 + (((px `1) / (px `2)) ^2)) by A26, A25, XREAL_1:64;
then ((px `2) ^2) + ((px `1) ^2) <= 1 + (((px `1) / (px `2)) ^2) by A26, XCMPLX_1:87;
then ((px `2) ^2) + ((px `1) ^2) <= 1 + (((px `1) ^2) / ((px `2) ^2)) by XCMPLX_1:76;
then (((px `2) ^2) + ((px `1) ^2)) - 1 <= (1 + (((px `1) ^2) / ((px `2) ^2))) - 1 by XREAL_1:9;
then ((((px `2) ^2) + ((px `1) ^2)) - 1) * ((px `2) ^2) <= (((px `1) ^2) / ((px `2) ^2)) * ((px `2) ^2) by A20, XREAL_1:64;
then (((px `2) ^2) * ((px `2) ^2)) + ((((px `1) ^2) - 1) * ((px `2) ^2)) <= (px `1) ^2 by A21, XCMPLX_1:6, XCMPLX_1:87;
then (((((px `2) ^2) * ((px `2) ^2)) - (((px `2) ^2) * 1)) + (((px `2) ^2) * ((px `1) ^2))) - (1 * ((px `1) ^2)) <= 0 by XREAL_1:47;
then A27: (((px `2) ^2) - 1) * (((px `2) ^2) + ((px `1) ^2)) <= 0 ;
(px `1) ^2 >= 0 by XREAL_1:63;
then A28: ((px `2) ^2) - 1 <= 0 by A20, A27, A19, XREAL_1:129;
then ( - 1 <= px `2 & px `2 <= 1 ) by SQUARE_1:43;
then ( ( px `1 <= 1 & 1 >= - (px `1) ) or ( px `1 >= - 1 & - (px `1) >= - 1 ) ) by A18, XXREAL_0:2;
then ( ( px `1 <= 1 & - 1 <= - (- (px `1)) ) or ( px `1 >= - 1 & px `1 <= 1 ) ) by XREAL_1:24;
hence ( - 1 <= px `1 & px `1 <= 1 & - 1 <= px `2 & px `2 <= 1 ) by A28, SQUARE_1:43; :: thesis: verum
end;
end;
end;
hence x in K0 by A1; :: thesis: verum