let D be Subset of (TOP-REAL 2); :: thesis: for K0 being Subset of ((TOP-REAL 2) | D) st K0 = { p where p is Point of (TOP-REAL 2) : ( ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ) & p <> 0. (TOP-REAL 2) ) } holds
rng (Out_In_Sq | K0) c= the carrier of (((TOP-REAL 2) | D) | K0)
let K0 be Subset of ((TOP-REAL 2) | D); :: thesis: ( K0 = { p where p is Point of (TOP-REAL 2) : ( ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ) & p <> 0. (TOP-REAL 2) ) } implies rng (Out_In_Sq | K0) c= the carrier of (((TOP-REAL 2) | D) | K0) )
assume A1: K0 = { p where p is Point of (TOP-REAL 2) : ( ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ) & p <> 0. (TOP-REAL 2) ) } ; :: thesis: rng (Out_In_Sq | K0) c= the carrier of (((TOP-REAL 2) | D) | K0)
A2: the carrier of ((TOP-REAL 2) | D) = [#] ((TOP-REAL 2) | D)
.= D by PRE_TOPC:def 10 ;
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (Out_In_Sq | K0) or y in the carrier of (((TOP-REAL 2) | D) | K0) )
assume y in rng (Out_In_Sq | K0) ; :: thesis: y in the carrier of (((TOP-REAL 2) | D) | K0)
then consider x being set such that
A3: ( x in dom (Out_In_Sq | K0) & y = (Out_In_Sq | K0) . x ) by FUNCT_1:def 5;
A4: x in (dom Out_In_Sq ) /\ K0 by A3, RELAT_1:90;
then A5: x in K0 by XBOOLE_0:def 4;
K0 c= the carrier of (TOP-REAL 2) by A2, XBOOLE_1:1;
then reconsider p = x as Point of (TOP-REAL 2) by A5;
A6: Out_In_Sq . p = y by A3, A5, FUNCT_1:72;
consider px being Point of (TOP-REAL 2) such that
A7: ( x = px & ( ( px `2 <= px `1 & - (px `1 ) <= px `2 ) or ( px `2 >= px `1 & px `2 <= - (px `1 ) ) ) & px <> 0. (TOP-REAL 2) ) by A1, A5;
reconsider K00 = K0 as Subset of (TOP-REAL 2) by A2, XBOOLE_1:1;
K00 = [#] ((TOP-REAL 2) | K00) by PRE_TOPC:def 10
.= the carrier of ((TOP-REAL 2) | K00) ;
then A8: p in the carrier of ((TOP-REAL 2) | K00) by A4, XBOOLE_0:def 4;
A9: for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K00) holds
q `1 <> 0

proof

let q be Point of (TOP-REAL 2); :: thesis: ( q in the carrier of ((TOP-REAL 2) | K00) implies q `1 <> 0 )
assume A10: q in the carrier of ((TOP-REAL 2) | K00) ; :: thesis: q `1 <> 0
the carrier of ((TOP-REAL 2) | K00) = [#] ((TOP-REAL 2) | K00)
.= K0 by PRE_TOPC:def 10 ;
then consider p3 being Point of (TOP-REAL 2) such that
A11: ( q = p3 & ( ( p3 `2 <= p3 `1 & - (p3 `1 ) <= p3 `2 ) or ( p3 `2 >= p3 `1 & p3 `2 <= - (p3 `1 ) ) ) & p3 <> 0. (TOP-REAL 2) ) by A1, A10;

now

assume A12: q `1 = 0 ; :: thesis: contradiction
then q `2 = 0 by A11;
hence contradiction by A11, A12, EUCLID:57, EUCLID:58; :: thesis: verum

end;

hence q `1 <> 0 ; :: thesis: verum

end;

then A13: p `1 <> 0 by A8;
set p9 = |[(1 / (p `1 )),(((p `2 ) / (p `1 )) / (p `1 ))]|;
A14: ( |[(1 / (p `1 )),(((p `2 ) / (p `1 )) / (p `1 ))]| `1 = 1 / (p `1 ) & |[(1 / (p `1 )),(((p `2 ) / (p `1 )) / (p `1 ))]| `2 = ((p `2 ) / (p `1 )) / (p `1 ) ) by EUCLID:56;

A15: now

assume |[(1 / (p `1 )),(((p `2 ) / (p `1 )) / (p `1 ))]| = 0. (TOP-REAL 2) ; :: thesis: contradiction
then 0 * (p `1 ) = (1 / (p `1 )) * (p `1 ) by A14, EUCLID:56, EUCLID:58;
hence contradiction by A8, A9, XCMPLX_1:88; :: thesis: verum

end;

A16: Out_In_Sq . p = |[(1 / (p `1 )),(((p `2 ) / (p `1 )) / (p `1 ))]| by A7, Def1;

now

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

case A17: p `1 >= 0 ; :: thesis: y in K0

then ( ( (p `2 ) / (p `1 ) <= (p `1 ) / (p `1 ) & (- (1 * (p `1 ))) / (p `1 ) <= (p `2 ) / (p `1 ) ) or ( p `2 >= p `1 & p `2 <= - (1 * (p `1 )) ) ) by A7, XREAL_1:74;
then B18: ( ( (p `2 ) / (p `1 ) <= 1 & ((- 1) * (p `1 )) / (p `1 ) <= (p `2 ) / (p `1 ) ) or ( p `2 >= p `1 & p `2 <= - (1 * (p `1 )) ) ) by A8, A9, XCMPLX_1:60;
then ( ( (p `2 ) / (p `1 ) <= 1 & - 1 <= (p `2 ) / (p `1 ) ) or ( (p `2 ) / (p `1 ) >= 1 & (p `2 ) / (p `1 ) <= ((- 1) * (p `1 )) / (p `1 ) ) ) by A13, A17, XCMPLX_1:90;
then (- 1) / (p `1 ) <= ((p `2 ) / (p `1 )) / (p `1 ) by A17, XREAL_1:74;
then A19: ( ( ((p `2 ) / (p `1 )) / (p `1 ) <= 1 / (p `1 ) & - (1 / (p `1 )) <= ((p `2 ) / (p `1 )) / (p `1 ) ) or ( ((p `2 ) / (p `1 )) / (p `1 ) >= 1 / (p `1 ) & ((p `2 ) / (p `1 )) / (p `1 ) <= - (1 / (p `1 )) ) ) by A17, B18, A13, XREAL_1:74;
( |[(1 / (p `1 )),(((p `2 ) / (p `1 )) / (p `1 ))]| `1 = 1 / (p `1 ) & |[(1 / (p `1 )),(((p `2 ) / (p `1 )) / (p `1 ))]| `2 = ((p `2 ) / (p `1 )) / (p `1 ) ) by EUCLID:56;
hence y in K0 by A1, A6, A15, A16, A19; :: thesis: verum

end;

case A20: p `1 < 0 ; :: thesis: y in K0

then ( ( p `2 <= p `1 & - (1 * (p `1 )) <= p `2 ) or ( (p `2 ) / (p `1 ) <= (p `1 ) / (p `1 ) & (p `2 ) / (p `1 ) >= (- (1 * (p `1 ))) / (p `1 ) ) ) by A7, XREAL_1:75;
then B21: ( ( p `2 <= p `1 & - (1 * (p `1 )) <= p `2 ) or ( (p `2 ) / (p `1 ) <= 1 & (p `2 ) / (p `1 ) >= ((- 1) * (p `1 )) / (p `1 ) ) ) by A20, XCMPLX_1:60;
then A21: ( ( (p `2 ) / (p `1 ) >= (p `1 ) / (p `1 ) & - (1 * (p `1 )) <= p `2 ) or ( (p `2 ) / (p `1 ) <= 1 & (p `2 ) / (p `1 ) >= - 1 ) ) by A20, XCMPLX_1:90;
( not (p `2 ) / (p `1 ) >= 1 or not (p `2 ) / (p `1 ) <= - 1 ) ;
then (- 1) / (p `1 ) >= ((p `2 ) / (p `1 )) / (p `1 ) by A20, A21, XCMPLX_1:60, XREAL_1:75;
then A23: ( ( ((p `2 ) / (p `1 )) / (p `1 ) <= 1 / (p `1 ) & - (1 / (p `1 )) <= ((p `2 ) / (p `1 )) / (p `1 ) ) or ( ((p `2 ) / (p `1 )) / (p `1 ) >= 1 / (p `1 ) & ((p `2 ) / (p `1 )) / (p `1 ) <= - (1 / (p `1 )) ) ) by A20, B21, XREAL_1:75;
( |[(1 / (p `1 )),(((p `2 ) / (p `1 )) / (p `1 ))]| `1 = 1 / (p `1 ) & |[(1 / (p `1 )),(((p `2 ) / (p `1 )) / (p `1 ))]| `2 = ((p `2 ) / (p `1 )) / (p `1 ) ) by EUCLID:56;
hence y in K0 by A1, A6, A15, A16, A23; :: thesis: verum

end;

end;

end;

then y in [#] (((TOP-REAL 2) | D) | K0) by PRE_TOPC:def 10;
hence y in the carrier of (((TOP-REAL 2) | D) | K0) ; :: thesis: verum