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 reconsider px = x as Point of (TOP-REAL 2) ;
set q = px;
A3: Sq_Circ . x in C0 by A2, FUNCT_1:def 13;
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 )
A5: 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;
A6: (px `1 ) ^2 >= 0 by XREAL_1:65;
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:56;
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:111;
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: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 A13, SQUARE_1:def 4
.= (((px `1 ) ^2 ) / (1 + (((px `2 ) / (px `1 )) ^2 ))) + (((px `2 ) ^2 ) / (1 + (((px `2 ) / (px `1 )) ^2 ))) by A13, 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 A13, A12, XREAL_1:66;
then ((px `1 ) ^2 ) + ((px `2 ) ^2 ) <= 1 + (((px `2 ) / (px `1 )) ^2 ) by A13, 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 A6, XREAL_1:66;
then (((px `1 ) ^2 ) * ((px `1 ) ^2 )) + ((((px `2 ) ^2 ) - 1) * ((px `1 ) ^2 )) <= (px `2 ) ^2 by A7, 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 A14: (((px `1 ) ^2 ) - 1) * (((px `1 ) ^2 ) + ((px `2 ) ^2 )) <= 0 ;
(px `2 ) ^2 >= 0 by XREAL_1:65;
then A15: ((px `1 ) ^2 ) - 1 <= 0 by A6, A14, A5, XREAL_1:131;
then A16: px `1 <= 1 by SQUARE_1:112;
A17: - 1 <= px `1 by A15, SQUARE_1:112;
then ( ( px `2 <= 1 & - (- (px `1 )) >= - (px `2 ) ) or ( px `2 >= - 1 & - (px `2 ) >= - (- (px `1 )) ) ) by A4, A16, 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 A17, 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 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
assume ((px `2 ) ^2 ) + ((px `1 ) ^2 ) = 0 ; :: thesis: contradiction
then px `2 = 0 by COMPLEX1:2;
hence contradiction by A18; :: thesis: verum
end;
A20: (px `2 ) ^2 >= 0 by XREAL_1:65;
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:56;
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:111;
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: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 A26, SQUARE_1:def 4
.= (((px `2 ) ^2 ) / (1 + (((px `1 ) / (px `2 )) ^2 ))) + (((px `1 ) ^2 ) / (1 + (((px `1 ) / (px `2 )) ^2 ))) by A26, 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 A26, A25, XREAL_1:66;
then ((px `2 ) ^2 ) + ((px `1 ) ^2 ) <= 1 + (((px `1 ) / (px `2 )) ^2 ) by A26, 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 A20, XREAL_1:66;
then (((px `2 ) ^2 ) * ((px `2 ) ^2 )) + ((((px `1 ) ^2 ) - 1) * ((px `2 ) ^2 )) <= (px `1 ) ^2 by A21, 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 A27: (((px `2 ) ^2 ) - 1) * (((px `2 ) ^2 ) + ((px `1 ) ^2 )) <= 0 ;
(px `1 ) ^2 >= 0 by XREAL_1:65;
then A28: ((px `2 ) ^2 ) - 1 <= 0 by A20, A27, A19, 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 A18, 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