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 set ; :: 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 A3: ( x in dom Sq_Circ & Sq_Circ . x in C0 ) by FUNCT_1:def 13;
reconsider px = x as Point of (TOP-REAL 2) by A2;
set q = px;
now
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:11; :: 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 )
then A5: Sq_Circ . px = |[((px `1 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))),((px `2 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))))]| by Def1;
A6: ( |[((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:56;
A7: (px `1 ) ^2 >= 0 by XREAL_1:65;
A8: 1 + (((px `2 ) / (px `1 )) ^2 ) > 0 by Lm1;
consider p1 being Point of (TOP-REAL 2) such that
A9: ( p1 = Sq_Circ . px & |.p1.| <= 1 ) by A1, A3;
|.p1.| ^2 <= |.p1.| by A9, SQUARE_1:111;
then A10: |.p1.| ^2 <= 1 by A9, XXREAL_0:2;
|.p1.| ^2 = (((px `1 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))) ^2 ) + (((px `2 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))) ^2 ) by A5, A6, A9, JGRAPH_1:46
.= (((px `1 ) ^2 ) / ((sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))) ^2 )) + (((px `2 ) / (sqrt (1 + (((px `2 ) / (px `1 )) ^2 )))) ^2 ) by XCMPLX_1:77
.= (((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:77
.= (((px `1 ) ^2 ) / (1 + (((px `2 ) / (px `1 )) ^2 ))) + (((px `2 ) ^2 ) / ((sqrt (1 + (((px `2 ) / (px `1 )) ^2 ))) ^2 )) by A8, SQUARE_1:def 4
.= (((px `1 ) ^2 ) / (1 + (((px `2 ) / (px `1 )) ^2 ))) + (((px `2 ) ^2 ) / (1 + (((px `2 ) / (px `1 )) ^2 ))) by A8, SQUARE_1:def 4
.= (((px `1 ) ^2 ) + ((px `2 ) ^2 )) / (1 + (((px `2 ) / (px `1 )) ^2 )) by XCMPLX_1:63 ;
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 A8, A10, XREAL_1:66;
then ((px `1 ) ^2 ) + ((px `2 ) ^2 ) <= 1 + (((px `2 ) / (px `1 )) ^2 ) by A8, XCMPLX_1:88;
then ((px `1 ) ^2 ) + ((px `2 ) ^2 ) <= 1 + (((px `2 ) ^2 ) / ((px `1 ) ^2 )) by XCMPLX_1:77;
then (((px `1 ) ^2 ) + ((px `2 ) ^2 )) - 1 <= (1 + (((px `2 ) ^2 ) / ((px `1 ) ^2 ))) - 1 by XREAL_1:11;
then ((((px `1 ) ^2 ) + ((px `2 ) ^2 )) - 1) * ((px `1 ) ^2 ) <= (((px `2 ) ^2 ) / ((px `1 ) ^2 )) * ((px `1 ) ^2 ) by A7, XREAL_1:66;
then (((px `1 ) ^2 ) * ((px `1 ) ^2 )) + ((((px `2 ) ^2 ) - 1) * ((px `1 ) ^2 )) <= (px `2 ) ^2 by A11, XCMPLX_1:6, XCMPLX_1:88;
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:49;
then A13: (((px `1 ) ^2 ) - 1) * (((px `1 ) ^2 ) + ((px `2 ) ^2 )) <= 0 ;
A14: now
assume ((px `1 ) ^2 ) + ((px `2 ) ^2 ) = 0 ; :: thesis: contradiction
then ( px `1 = 0 & px `2 = 0 ) by COMPLEX1:2;
hence contradiction by A4, EUCLID:57, EUCLID:58; :: thesis: verum
end;
(px `2 ) ^2 >= 0 by XREAL_1:65;
then ((px `1 ) ^2 ) + ((px `2 ) ^2 ) >= 0 + 0 by A7;
then A15: ((px `1 ) ^2 ) - 1 <= 0 by A13, A14, XREAL_1:131;
then A16: ( - 1 <= px `1 & px `1 <= 1 ) by SQUARE_1:112;
then ( ( px `2 <= 1 & - (- (px `1 )) >= - (px `2 ) ) or ( px `2 >= - 1 & - (px `2 ) >= - (- (px `1 )) ) ) by A4, XREAL_1:26, 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 A16, XREAL_1:26, XXREAL_0:2;
hence ( - 1 <= px `1 & px `1 <= 1 & - 1 <= px `2 & px `2 <= 1 ) by A15, SQUARE_1:112, XREAL_1:26; :: thesis: verum
end;
case A17: ( 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 )
then A18: Sq_Circ . px = |[((px `1 ) / (sqrt (1 + (((px `1 ) / (px `2 )) ^2 )))),((px `2 ) / (sqrt (1 + (((px `1 ) / (px `2 )) ^2 ))))]| by Def1;
A19: ( |[((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:56;
A21: (px `2 ) ^2 >= 0 by XREAL_1:65;
A22: 1 + (((px `1 ) / (px `2 )) ^2 ) > 0 by Lm1;
consider p1 being Point of (TOP-REAL 2) such that
A23: ( p1 = Sq_Circ . px & |.p1.| <= 1 ) by A1, A3;
|.p1.| ^2 <= |.p1.| by A23, SQUARE_1:111;
then A24: |.p1.| ^2 <= 1 by A23, XXREAL_0:2;
A25: px `2 <> 0 by A17;
|.p1.| ^2 = (((px `1 ) / (sqrt (1 + (((px `1 ) / (px `2 )) ^2 )))) ^2 ) + (((px `2 ) / (sqrt (1 + (((px `1 ) / (px `2 )) ^2 )))) ^2 ) by A18, A19, A23, JGRAPH_1:46
.= (((px `2 ) ^2 ) / ((sqrt (1 + (((px `1 ) / (px `2 )) ^2 ))) ^2 )) + (((px `1 ) / (sqrt (1 + (((px `1 ) / (px `2 )) ^2 )))) ^2 ) by XCMPLX_1:77
.= (((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:77
.= (((px `2 ) ^2 ) / (1 + (((px `1 ) / (px `2 )) ^2 ))) + (((px `1 ) ^2 ) / ((sqrt (1 + (((px `1 ) / (px `2 )) ^2 ))) ^2 )) by A22, SQUARE_1:def 4
.= (((px `2 ) ^2 ) / (1 + (((px `1 ) / (px `2 )) ^2 ))) + (((px `1 ) ^2 ) / (1 + (((px `1 ) / (px `2 )) ^2 ))) by A22, SQUARE_1:def 4
.= (((px `2 ) ^2 ) + ((px `1 ) ^2 )) / (1 + (((px `1 ) / (px `2 )) ^2 )) by XCMPLX_1:63 ;
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 A22, A24, XREAL_1:66;
then ((px `2 ) ^2 ) + ((px `1 ) ^2 ) <= 1 + (((px `1 ) / (px `2 )) ^2 ) by A22, XCMPLX_1:88;
then ((px `2 ) ^2 ) + ((px `1 ) ^2 ) <= 1 + (((px `1 ) ^2 ) / ((px `2 ) ^2 )) by XCMPLX_1:77;
then (((px `2 ) ^2 ) + ((px `1 ) ^2 )) - 1 <= (1 + (((px `1 ) ^2 ) / ((px `2 ) ^2 ))) - 1 by XREAL_1:11;
then ((((px `2 ) ^2 ) + ((px `1 ) ^2 )) - 1) * ((px `2 ) ^2 ) <= (((px `1 ) ^2 ) / ((px `2 ) ^2 )) * ((px `2 ) ^2 ) by A21, XREAL_1:66;
then (((px `2 ) ^2 ) * ((px `2 ) ^2 )) + ((((px `1 ) ^2 ) - 1) * ((px `2 ) ^2 )) <= (px `1 ) ^2 by A25, XCMPLX_1:6, XCMPLX_1:88;
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:49;
then A26: (((px `2 ) ^2 ) - 1) * (((px `2 ) ^2 ) + ((px `1 ) ^2 )) <= 0 ;
A27: now
assume ((px `2 ) ^2 ) + ((px `1 ) ^2 ) = 0 ; :: thesis: contradiction
then ( px `2 = 0 & px `1 = 0 ) by COMPLEX1:2;
hence contradiction by A17; :: thesis: verum
end;
(px `1 ) ^2 >= 0 by XREAL_1:65;
then ((px `2 ) ^2 ) + ((px `1 ) ^2 ) >= 0 + 0 by A21;
then A28: ((px `2 ) ^2 ) - 1 <= 0 by A26, A27, XREAL_1:131;
then ( - 1 <= px `2 & px `2 <= 1 ) by SQUARE_1:112;
then ( ( px `1 <= 1 & 1 >= - (px `1 ) ) or ( px `1 >= - 1 & - (px `1 ) >= - 1 ) ) by A17, XXREAL_0:2;
then ( ( px `1 <= 1 & - 1 <= - (- (px `1 )) ) or ( px `1 >= - 1 & px `1 <= 1 ) ) by XREAL_1:26;
hence ( - 1 <= px `1 & px `1 <= 1 & - 1 <= px `2 & px `2 <= 1 ) by A28, SQUARE_1:112; :: thesis: verum
end;
end;
end;
hence x in K0 by A1; :: thesis: verum