let B0 be Subset of (TOP-REAL 2); :: thesis: for K0 being Subset of ((TOP-REAL 2) | B0)
for f being Function of (((TOP-REAL 2) | B0) | K0),((TOP-REAL 2) | B0) st f = Out_In_Sq | K0 & B0 = NonZero (TOP-REAL 2) & 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
( f is continuous & K0 is closed )
let K0 be Subset of ((TOP-REAL 2) | B0); :: thesis: for f being Function of (((TOP-REAL 2) | B0) | K0),((TOP-REAL 2) | B0) st f = Out_In_Sq | K0 & B0 = NonZero (TOP-REAL 2) & 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
( f is continuous & K0 is closed )
let f be Function of (((TOP-REAL 2) | B0) | K0),((TOP-REAL 2) | B0); :: thesis: ( f = Out_In_Sq | K0 & B0 = NonZero (TOP-REAL 2) & 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 ( f is continuous & K0 is closed ) )
assume A1: ( f = Out_In_Sq | K0 & B0 = NonZero (TOP-REAL 2) & 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: ( f is continuous & K0 is closed )
the carrier of ((TOP-REAL 2) | B0) = [#] ((TOP-REAL 2) | B0)
.= B0 by PRE_TOPC:def 10 ;
then reconsider K1 = K0 as Subset of (TOP-REAL 2) by XBOOLE_1:1;
K0 c= B0

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in K0 or x in B0 )
assume x in K0 ; :: thesis: x in B0
then consider p8 being Point of (TOP-REAL 2) such that
A2: ( x = p8 & ( ( p8 `1 <= p8 `2 & - (p8 `2 ) <= p8 `1 ) or ( p8 `1 >= p8 `2 & p8 `1 <= - (p8 `2 ) ) ) & p8 <> 0. (TOP-REAL 2) ) by A1;
( x in the carrier of (TOP-REAL 2) & not x in {(0. (TOP-REAL 2))} ) by A2, TARSKI:def 1;
hence x in B0 by A1, XBOOLE_0:def 5; :: thesis: verum

end;

then A3: ((TOP-REAL 2) | B0) | K0 = (TOP-REAL 2) | K1 by PRE_TOPC:28;
defpred S₁[ Point of (TOP-REAL 2)] means ( ( $1 `1 <= $1 `2 & - ($1 `2 ) <= $1 `1 ) or ( $1 `1 >= $1 `2 & $1 `1 <= - ($1 `2 ) ) );
reconsider K1 = { p7 where p7 is Point of (TOP-REAL 2) : S₁[p7] } as Subset of (TOP-REAL 2) from JGRAPH_2:sch 1();
reconsider K2 = { p7 where p7 is Point of (TOP-REAL 2) : p7 `1 <= p7 `2 } as closed Subset of (TOP-REAL 2) by Lm4;
reconsider K3 = { p7 where p7 is Point of (TOP-REAL 2) : - (p7 `2 ) <= p7 `1 } as closed Subset of (TOP-REAL 2) by Lm16;
reconsider K4 = { p7 where p7 is Point of (TOP-REAL 2) : p7 `2 <= p7 `1 } as closed Subset of (TOP-REAL 2) by Lm7;
reconsider K5 = { p7 where p7 is Point of (TOP-REAL 2) : p7 `1 <= - (p7 `2 ) } as closed Subset of (TOP-REAL 2) by Lm19;
A4: K2 /\ K3 is closed by TOPS_1:35;
A5: K4 /\ K5 is closed by TOPS_1:35;
A6: (K2 /\ K3) \/ (K4 /\ K5) c= K1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (K2 /\ K3) \/ (K4 /\ K5) or x in K1 )
assume A7: x in (K2 /\ K3) \/ (K4 /\ K5) ; :: thesis: x in K1

now

per cases ( x in K2 /\ K3 or x in K4 /\ K5 ) by A7, XBOOLE_0:def 3;

case x in K2 /\ K3 ; :: thesis: x in K1

then A8: ( x in K2 & x in K3 ) by XBOOLE_0:def 4;
then consider p7 being Point of (TOP-REAL 2) such that
A9: ( p7 = x & p7 `1 <= p7 `2 ) ;
consider p8 being Point of (TOP-REAL 2) such that
A10: ( p8 = x & - (p8 `2 ) <= p8 `1 ) by A8;
thus x in K1 by A9, A10; :: thesis: verum

end;

case x in K4 /\ K5 ; :: thesis: x in K1

then A11: ( x in K4 & x in K5 ) by XBOOLE_0:def 4;
then consider p7 being Point of (TOP-REAL 2) such that
A12: ( p7 = x & p7 `1 >= p7 `2 ) ;
consider p8 being Point of (TOP-REAL 2) such that
A13: ( p8 = x & p8 `1 <= - (p8 `2 ) ) by A11;
thus x in K1 by A12, A13; :: thesis: verum

end;

end;

end;

hence x in K1 ; :: thesis: verum

end;

K1 c= (K2 /\ K3) \/ (K4 /\ K5)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in K1 or x in (K2 /\ K3) \/ (K4 /\ K5) )
assume x in K1 ; :: thesis: x in (K2 /\ K3) \/ (K4 /\ K5)
then consider p being Point of (TOP-REAL 2) such that
A14: ( p = x & ( ( p `1 <= p `2 & - (p `2 ) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2 ) ) ) ) ;
( ( x in K2 & x in K3 ) or ( x in K4 & x in K5 ) ) by A14;
then ( x in K2 /\ K3 or x in K4 /\ K5 ) by XBOOLE_0:def 4;
hence x in (K2 /\ K3) \/ (K4 /\ K5) by XBOOLE_0:def 3; :: thesis: verum

end;

then K1 = (K2 /\ K3) \/ (K4 /\ K5) by A6, XBOOLE_0:def 10;
then A15: K1 is closed by A4, A5, TOPS_1:36;
A16: K1 /\ B0 c= K0

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in K1 /\ B0 or x in K0 )
assume x in K1 /\ B0 ; :: thesis: x in K0
then A17: ( x in K1 & x in B0 ) by XBOOLE_0:def 4;
then consider p7 being Point of (TOP-REAL 2) such that
A18: ( p7 = x & ( ( p7 `1 <= p7 `2 & - (p7 `2 ) <= p7 `1 ) or ( p7 `1 >= p7 `2 & p7 `1 <= - (p7 `2 ) ) ) ) ;
( x in the carrier of (TOP-REAL 2) & not x in {(0. (TOP-REAL 2))} ) by A1, A17, XBOOLE_0:def 5;
then not x = 0. (TOP-REAL 2) by TARSKI:def 1;
hence x in K0 by A1, A18; :: thesis: verum

end;

K0 c= K1 /\ B0

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in K0 or x in K1 /\ B0 )
assume x in K0 ; :: thesis: x in K1 /\ B0
then consider p being Point of (TOP-REAL 2) such that
A19: ( x = p & ( ( p `1 <= p `2 & - (p `2 ) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2 ) ) ) & p <> 0. (TOP-REAL 2) ) by A1;
( x in the carrier of (TOP-REAL 2) & not x in {(0. (TOP-REAL 2))} ) by A19, TARSKI:def 1;
then ( x in K1 & x in B0 ) by A1, A19, XBOOLE_0:def 5;
hence x in K1 /\ B0 by XBOOLE_0:def 4; :: thesis: verum

end;

then K0 = K1 /\ B0 by A16, XBOOLE_0:def 10
.= K1 /\ ([#] ((TOP-REAL 2) | B0)) by PRE_TOPC:def 10 ;
hence ( f is continuous & K0 is closed ) by A1, A3, A15, Th47, PRE_TOPC:43; :: thesis: verum