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 `1 <= p `2 & - (p `2 ) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2 ) ) ) & 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 `1 <= p `2 & - (p `2 ) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2 ) ) ) & 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 `1 <= p `2 & - (p `2 ) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2 ) ) ) & 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;
x in (dom Out_In_Sq ) /\ K0 by A3, RELAT_1:90;
then A4: 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 A4;
A5: Out_In_Sq . p = y by A3, A4, FUNCT_1:72;
consider px being Point of (TOP-REAL 2) such that
A6: ( x = px & ( ( px `1 <= px `2 & - (px `2 ) <= px `1 ) or ( px `1 >= px `2 & px `1 <= - (px `2 ) ) ) & px <> 0. (TOP-REAL 2) ) by A1, A4;
reconsider K00 = K0 as Subset of (TOP-REAL 2) by A2, XBOOLE_1:1;
A7: K00 = [#] ((TOP-REAL 2) | K00) by PRE_TOPC:def 10
.= the carrier of ((TOP-REAL 2) | K00) ;
A8: for q being Point of (TOP-REAL 2) st q in the carrier of ((TOP-REAL 2) | K00) holds
q `2 <> 0

proof

let q be Point of (TOP-REAL 2); :: thesis: ( q in the carrier of ((TOP-REAL 2) | K00) implies q `2 <> 0 )
assume A9: q in the carrier of ((TOP-REAL 2) | K00) ; :: thesis: q `2 <> 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
A10: ( q = p3 & ( ( p3 `1 <= p3 `2 & - (p3 `2 ) <= p3 `1 ) or ( p3 `1 >= p3 `2 & p3 `1 <= - (p3 `2 ) ) ) & p3 <> 0. (TOP-REAL 2) ) by A1, A9;

now

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

end;

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

end;

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

A14: now

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

end;

A15: Out_In_Sq . p = |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]| by A6, Th24;

now

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

case A16: p `2 >= 0 ; :: thesis: y in K0

then ( ( (p `1 ) / (p `2 ) <= (p `2 ) / (p `2 ) & (- (1 * (p `2 ))) / (p `2 ) <= (p `1 ) / (p `2 ) ) or ( p `1 >= p `2 & p `1 <= - (1 * (p `2 )) ) ) by A6, XREAL_1:74;
then B17: ( ( (p `1 ) / (p `2 ) <= 1 & ((- 1) * (p `2 )) / (p `2 ) <= (p `1 ) / (p `2 ) ) or ( p `1 >= p `2 & p `1 <= - (1 * (p `2 )) ) ) by A4, A7, A8, XCMPLX_1:60;
then ( ( (p `1 ) / (p `2 ) <= 1 & - 1 <= (p `1 ) / (p `2 ) ) or ( (p `1 ) / (p `2 ) >= 1 & (p `1 ) / (p `2 ) <= ((- 1) * (p `2 )) / (p `2 ) ) ) by A12, A16, XCMPLX_1:90;
then (- 1) / (p `2 ) <= ((p `1 ) / (p `2 )) / (p `2 ) by A16, XREAL_1:74;
then A18: ( ( ((p `1 ) / (p `2 )) / (p `2 ) <= 1 / (p `2 ) & - (1 / (p `2 )) <= ((p `1 ) / (p `2 )) / (p `2 ) ) or ( ((p `1 ) / (p `2 )) / (p `2 ) >= 1 / (p `2 ) & ((p `1 ) / (p `2 )) / (p `2 ) <= - (1 / (p `2 )) ) ) by A16, B17, A12, XREAL_1:74;
( |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]| `2 = 1 / (p `2 ) & |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]| `1 = ((p `1 ) / (p `2 )) / (p `2 ) ) by EUCLID:56;
hence y in K0 by A1, A5, A14, A15, A18; :: thesis: verum

end;

case A19: p `2 < 0 ; :: thesis: y in K0

then ( ( p `1 <= p `2 & - (1 * (p `2 )) <= p `1 ) or ( (p `1 ) / (p `2 ) <= (p `2 ) / (p `2 ) & (p `1 ) / (p `2 ) >= (- (1 * (p `2 ))) / (p `2 ) ) ) by A6, XREAL_1:75;
then B20: ( ( p `1 <= p `2 & - (1 * (p `2 )) <= p `1 ) or ( (p `1 ) / (p `2 ) <= 1 & (p `1 ) / (p `2 ) >= ((- 1) * (p `2 )) / (p `2 ) ) ) by A19, XCMPLX_1:60;
then ( ( (p `1 ) / (p `2 ) >= 1 & ((- 1) * (p `2 )) / (p `2 ) >= (p `1 ) / (p `2 ) ) or ( (p `1 ) / (p `2 ) <= 1 & (p `1 ) / (p `2 ) >= - 1 ) ) by A19, XCMPLX_1:90;
then (- 1) / (p `2 ) >= ((p `1 ) / (p `2 )) / (p `2 ) by A19, XREAL_1:75;
then A21: ( ( ((p `1 ) / (p `2 )) / (p `2 ) <= 1 / (p `2 ) & - (1 / (p `2 )) <= ((p `1 ) / (p `2 )) / (p `2 ) ) or ( ((p `1 ) / (p `2 )) / (p `2 ) >= 1 / (p `2 ) & ((p `1 ) / (p `2 )) / (p `2 ) <= - (1 / (p `2 )) ) ) by A19, B20, XREAL_1:75;
( |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]| `2 = 1 / (p `2 ) & |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]| `1 = ((p `1 ) / (p `2 )) / (p `2 ) ) by EUCLID:56;
hence y in K0 by A1, A5, A14, A15, A21; :: 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