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) )
A1: the carrier of ((TOP-REAL 2) | D) = [#] ((TOP-REAL 2) | D)
.= D by PRE_TOPC:def 5 ;
then reconsider K00 = K0 as Subset of (TOP-REAL 2) by XBOOLE_1:1;
assume A2: 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)
A3: 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 )
A4: the carrier of ((TOP-REAL 2) | K00) = [#] ((TOP-REAL 2) | K00)
.= K0 by PRE_TOPC:def 5 ;
assume q in the carrier of ((TOP-REAL 2) | K00) ; :: thesis: q `1 <> 0
then A5: ex p3 being Point of (TOP-REAL 2) st
( 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 A2, A4;

now :: thesis: not q `1 = 0

assume A6: q `1 = 0 ; :: thesis: contradiction
then q `2 = 0 by A5;
hence contradiction by A5, A6, EUCLID:53, EUCLID:54; :: thesis: verum

end;

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

end;

let y be object ; :: 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 object such that
A7: x in dom (Out_In_Sq | K0) and
A8: y = (Out_In_Sq | K0) . x by FUNCT_1:def 3;
A9: x in (dom Out_In_Sq) /\ K0 by A7, RELAT_1:61;
then A10: x in K0 by XBOOLE_0:def 4;
K0 c= the carrier of (TOP-REAL 2) by A1, XBOOLE_1:1;
then reconsider p = x as Point of (TOP-REAL 2) by A10;
A11: Out_In_Sq . p = y by A8, A10, FUNCT_1:49;
A12: ex px being Point of (TOP-REAL 2) st
( 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 A2, A10;
then A13: Out_In_Sq . p = |[(1 / (p `1)),(((p `2) / (p `1)) / (p `1))]| by Def1;
set p9 = |[(1 / (p `1)),(((p `2) / (p `1)) / (p `1))]|;
K00 = [#] ((TOP-REAL 2) | K00) by PRE_TOPC:def 5
.= the carrier of ((TOP-REAL 2) | K00) ;
then A14: p in the carrier of ((TOP-REAL 2) | K00) by A9, XBOOLE_0:def 4;
A15: |[(1 / (p `1)),(((p `2) / (p `1)) / (p `1))]| `1 = 1 / (p `1) by EUCLID:52;

A16: now :: thesis: not |[(1 / (p `1)),(((p `2) / (p `1)) / (p `1))]| = 0. (TOP-REAL 2)

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 A15, EUCLID:52, EUCLID:54;
hence contradiction by A14, A3, XCMPLX_1:87; :: thesis: verum

end;

A17: p `1 <> 0 by A14, A3;

now :: thesis: y in K0

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

suppose A18: 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 A12, XREAL_1:72;
then A19: ( ( (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 A14, A3, 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 A17, A18, XCMPLX_1:89;
then (- 1) / (p `1) <= ((p `2) / (p `1)) / (p `1) by A18, XREAL_1:72;
then A20: ( ( ((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, A18, A19, XREAL_1:72;
( |[(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:52;
hence y in K0 by A2, A11, A16, A13, A20; :: thesis: verum

end;

suppose A21: p `1 < 0 ; :: thesis: y in K0

A22: now :: thesis: ( ( p `2 <= p `1 & - (1 * (p `1)) <= p `2 & ((p `2) / (p `1)) / (p `1) <= 1 / (p `1) & - (1 / (p `1)) <= ((p `2) / (p `1)) / (p `1) ) or ( p `2 >= p `1 & p `2 <= - (1 * (p `1)) & ((p `2) / (p `1)) / (p `1) >= 1 / (p `1) & - (1 / (p `1)) >= ((p `2) / (p `1)) / (p `1) ) )

per cases ( ( p `2 <= p `1 & - (1 * (p `1)) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (1 * (p `1)) ) ) by A12;

case that A23: p `2 <= p `1 and
A24: - (1 * (p `1)) <= p `2 ; :: thesis: ( ((p `2) / (p `1)) / (p `1) <= 1 / (p `1) & - (1 / (p `1)) <= ((p `2) / (p `1)) / (p `1) )

(p `2) / (p `1) >= 1 by A21, A23, XREAL_1:182;
hence ((p `2) / (p `1)) / (p `1) <= 1 / (p `1) by A21, XREAL_1:73; :: thesis: - (1 / (p `1)) <= ((p `2) / (p `1)) / (p `1)
(- 1) * (p `1) <= p `2 by A24;
then - 1 >= (p `2) / (p `1) by A21, XREAL_1:78;
then (- 1) / (p `1) <= ((p `2) / (p `1)) / (p `1) by A21, XREAL_1:73;
hence - (1 / (p `1)) <= ((p `2) / (p `1)) / (p `1) ; :: thesis: verum

end;

case that A25: p `2 >= p `1 and
A26: p `2 <= - (1 * (p `1)) ; :: thesis: ( ((p `2) / (p `1)) / (p `1) >= 1 / (p `1) & - (1 / (p `1)) >= ((p `2) / (p `1)) / (p `1) )

(p `2) / (p `1) <= 1 by A21, A25, XREAL_1:186;
hence ((p `2) / (p `1)) / (p `1) >= 1 / (p `1) by A21, XREAL_1:73; :: thesis: - (1 / (p `1)) >= ((p `2) / (p `1)) / (p `1)
(- 1) * (p `1) >= p `2 by A26;
then - 1 <= (p `2) / (p `1) by A21, XREAL_1:80;
then (- 1) / (p `1) >= ((p `2) / (p `1)) / (p `1) by A21, XREAL_1:73;
hence - (1 / (p `1)) >= ((p `2) / (p `1)) / (p `1) ; :: thesis: verum

end;

end;

end;

( |[(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:52;
hence y in K0 by A2, A11, A16, A13, A22; :: thesis: verum

end;

end;

end;

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