reconsider K5 = { p7 where p7 is Point of () : p7 `2 <= - (p7 `1) } as closed Subset of () by JGRAPH_2:47;
reconsider K4 = { p7 where p7 is Point of () : p7 `1 <= p7 `2 } as closed Subset of () by JGRAPH_2:46;
reconsider K3 = { p7 where p7 is Point of () : - (p7 `1) <= p7 `2 } as closed Subset of () by JGRAPH_2:47;
reconsider K2 = { p7 where p7 is Point of () : p7 `2 <= p7 `1 } as closed Subset of () by JGRAPH_2:46;
defpred S1[ Point of ()] means ( ( \$1 `2 <= \$1 `1 & - (\$1 `1) <= \$1 `2 ) or ( \$1 `2 >= \$1 `1 & \$1 `2 <= - (\$1 `1) ) );
let B0 be Subset of (); :: thesis: for K0 being Subset of (() | B0)
for f being Function of ((() | B0) | K0),(() | B0) st f = Sq_Circ | K0 & B0 = NonZero () & K0 = { p where p is Point of () : ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. () ) } holds
( f is continuous & K0 is closed )

let K0 be Subset of (() | B0); :: thesis: for f being Function of ((() | B0) | K0),(() | B0) st f = Sq_Circ | K0 & B0 = NonZero () & K0 = { p where p is Point of () : ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. () ) } holds
( f is continuous & K0 is closed )

let f be Function of ((() | B0) | K0),(() | B0); :: thesis: ( f = Sq_Circ | K0 & B0 = NonZero () & K0 = { p where p is Point of () : ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. () ) } implies ( f is continuous & K0 is closed ) )
assume A1: ( f = Sq_Circ | K0 & B0 = NonZero () & K0 = { p where p is Point of () : ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. () ) } ) ; :: thesis: ( f is continuous & K0 is closed )
the carrier of (() | B0) = B0 by PRE_TOPC:8;
then reconsider K1 = K0 as Subset of () by XBOOLE_1:1;
{ p where p is Point of () : ( S1[p] & p <> 0. () ) } c= NonZero () from then A2: ((TOP-REAL 2) | B0) | K0 = () | K1 by ;
defpred S2[ Point of ()] means ( ( \$1 `2 <= \$1 `1 & - (\$1 `1) <= \$1 `2 ) or ( \$1 `2 >= \$1 `1 & \$1 `2 <= - (\$1 `1) ) );
reconsider K1 = { p7 where p7 is Point of () : S2[p7] } as Subset of () from defpred S3[ Point of ()] means ( ( \$1 `2 <= \$1 `1 & - (\$1 `1) <= \$1 `2 ) or ( \$1 `2 >= \$1 `1 & \$1 `2 <= - (\$1 `1) ) );
{ p where p is Point of () : ( S3[p] & p <> 0. () ) } = { p7 where p7 is Point of () : S3[p7] } /\ (NonZero ()) from then A3: K0 = K1 /\ ([#] (() | B0)) by ;
A4: (K2 /\ K3) \/ (K4 /\ K5) c= K1
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (K2 /\ K3) \/ (K4 /\ K5) or x in K1 )
assume A5: x in (K2 /\ K3) \/ (K4 /\ K5) ; :: thesis: x in K1
per cases ( x in K2 /\ K3 or x in K4 /\ K5 ) by ;
suppose A6: x in K2 /\ K3 ; :: thesis: x in K1
then x in K3 by XBOOLE_0:def 4;
then A7: ex p8 being Point of () st
( p8 = x & - (p8 `1) <= p8 `2 ) ;
x in K2 by ;
then ex p7 being Point of () st
( p7 = x & p7 `2 <= p7 `1 ) ;
hence x in K1 by A7; :: thesis: verum
end;
suppose A8: x in K4 /\ K5 ; :: thesis: x in K1
then x in K5 by XBOOLE_0:def 4;
then A9: ex p8 being Point of () st
( p8 = x & p8 `2 <= - (p8 `1) ) ;
x in K4 by ;
then ex p7 being Point of () st
( p7 = x & p7 `2 >= p7 `1 ) ;
hence x in K1 by A9; :: thesis: verum
end;
end;
end;
A10: ( K2 /\ K3 is closed & K4 /\ K5 is closed ) by TOPS_1:8;
K1 c= (K2 /\ K3) \/ (K4 /\ K5)
proof
let x be object ; :: 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 ex p being Point of () st
( p = x & ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) ) ;
then ( ( x in K2 & x in K3 ) or ( x in K4 & x in K5 ) ) ;
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 A4;
then K1 is closed by ;
hence ( f is continuous & K0 is closed ) by ; :: thesis: verum