reconsider K5 = { p7 where p7 is Point of (TOP-REAL 2) : p7 `1 <= - (p7 `2) } as closed Subset of (TOP-REAL 2) by JGRAPH_2:48;

reconsider K4 = { p7 where p7 is Point of (TOP-REAL 2) : p7 `2 <= p7 `1 } as closed Subset of (TOP-REAL 2) by JGRAPH_2:46;

reconsider K3 = { p7 where p7 is Point of (TOP-REAL 2) : - (p7 `2) <= p7 `1 } as closed Subset of (TOP-REAL 2) by JGRAPH_2:48;

reconsider K2 = { p7 where p7 is Point of (TOP-REAL 2) : p7 `1 <= p7 `2 } as closed Subset of (TOP-REAL 2) by JGRAPH_2:46;

defpred S_{1}[ Point of (TOP-REAL 2)] means ( ( $1 `1 <= $1 `2 & - ($1 `2) <= $1 `1 ) or ( $1 `1 >= $1 `2 & $1 `1 <= - ($1 `2) ) );

defpred S_{2}[ Point of (TOP-REAL 2)] means ( ( $1 `1 <= $1 `2 & - ($1 `2) <= $1 `1 ) or ( $1 `1 >= $1 `2 & $1 `1 <= - ($1 `2) ) );

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 = (Sq_Circ ") | 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 = (Sq_Circ ") | 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 = (Sq_Circ ") | 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 ) )

set k0 = { p where p is Point of (TOP-REAL 2) : ( S_{2}[p] & p <> 0. (TOP-REAL 2) ) } ;

set b0 = NonZero (TOP-REAL 2);

assume that

A1: f = (Sq_Circ ") | K0 and

A2: ( B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( S_{2}[p] & p <> 0. (TOP-REAL 2) ) } )
; :: thesis: ( f is continuous & K0 is closed )

the carrier of ((TOP-REAL 2) | B0) = B0 by PRE_TOPC:8;

then reconsider K1 = K0 as Subset of (TOP-REAL 2) by XBOOLE_1:1;

{ p where p is Point of (TOP-REAL 2) : ( S_{1}[p] & p <> 0. (TOP-REAL 2) ) } c= NonZero (TOP-REAL 2)
from JGRAPH_3:sch 1();

then A3: ((TOP-REAL 2) | B0) | K0 = (TOP-REAL 2) | K1 by A2, PRE_TOPC:7;

set k1 = { p7 where p7 is Point of (TOP-REAL 2) : S_{2}[p7] } ;

A4: ( K2 /\ K3 is closed & K4 /\ K5 is closed ) by TOPS_1:8;

reconsider K1 = { p7 where p7 is Point of (TOP-REAL 2) : S_{2}[p7] } as Subset of (TOP-REAL 2) from JGRAPH_2:sch 1();

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

then A11: K1 is closed by A4, TOPS_1:9;

{ p where p is Point of (TOP-REAL 2) : ( S_{2}[p] & p <> 0. (TOP-REAL 2) ) } = { p7 where p7 is Point of (TOP-REAL 2) : S_{2}[p7] } /\ (NonZero (TOP-REAL 2))
from JGRAPH_3:sch 2();

then K0 = K1 /\ ([#] ((TOP-REAL 2) | B0)) by A2, PRE_TOPC:def 5;

hence ( f is continuous & K0 is closed ) by A1, A2, A3, A11, Th38, PRE_TOPC:13; :: thesis: verum

reconsider K4 = { p7 where p7 is Point of (TOP-REAL 2) : p7 `2 <= p7 `1 } as closed Subset of (TOP-REAL 2) by JGRAPH_2:46;

reconsider K3 = { p7 where p7 is Point of (TOP-REAL 2) : - (p7 `2) <= p7 `1 } as closed Subset of (TOP-REAL 2) by JGRAPH_2:48;

reconsider K2 = { p7 where p7 is Point of (TOP-REAL 2) : p7 `1 <= p7 `2 } as closed Subset of (TOP-REAL 2) by JGRAPH_2:46;

defpred S

defpred S

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 = (Sq_Circ ") | 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 = (Sq_Circ ") | 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 = (Sq_Circ ") | 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 ) )

set k0 = { p where p is Point of (TOP-REAL 2) : ( S

set b0 = NonZero (TOP-REAL 2);

assume that

A1: f = (Sq_Circ ") | K0 and

A2: ( B0 = NonZero (TOP-REAL 2) & K0 = { p where p is Point of (TOP-REAL 2) : ( S

the carrier of ((TOP-REAL 2) | B0) = B0 by PRE_TOPC:8;

then reconsider K1 = K0 as Subset of (TOP-REAL 2) by XBOOLE_1:1;

{ p where p is Point of (TOP-REAL 2) : ( S

then A3: ((TOP-REAL 2) | B0) | K0 = (TOP-REAL 2) | K1 by A2, PRE_TOPC:7;

set k1 = { p7 where p7 is Point of (TOP-REAL 2) : S

A4: ( K2 /\ K3 is closed & K4 /\ K5 is closed ) by TOPS_1:8;

reconsider K1 = { p7 where p7 is Point of (TOP-REAL 2) : S

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

proof

K1 c= (K2 /\ K3) \/ (K4 /\ K5)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (K2 /\ K3) \/ (K4 /\ K5) or x in K1 )

assume A6: x in (K2 /\ K3) \/ (K4 /\ K5) ; :: thesis: x in K1

end;assume A6: x in (K2 /\ K3) \/ (K4 /\ K5) ; :: thesis: x in K1

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

end;

suppose A7:
x in K2 /\ K3
; :: thesis: x in K1

then
x in K3
by XBOOLE_0:def 4;

then A8: ex p8 being Point of (TOP-REAL 2) st

( p8 = x & - (p8 `2) <= p8 `1 ) ;

x in K2 by A7, XBOOLE_0:def 4;

then ex p7 being Point of (TOP-REAL 2) st

( p7 = x & p7 `1 <= p7 `2 ) ;

hence x in K1 by A8; :: thesis: verum

end;then A8: ex p8 being Point of (TOP-REAL 2) st

( p8 = x & - (p8 `2) <= p8 `1 ) ;

x in K2 by A7, XBOOLE_0:def 4;

then ex p7 being Point of (TOP-REAL 2) st

( p7 = x & p7 `1 <= p7 `2 ) ;

hence x in K1 by A8; :: thesis: verum

suppose A9:
x in K4 /\ K5
; :: thesis: x in K1

then
x in K5
by XBOOLE_0:def 4;

then A10: ex p8 being Point of (TOP-REAL 2) st

( p8 = x & p8 `1 <= - (p8 `2) ) ;

x in K4 by A9, XBOOLE_0:def 4;

then ex p7 being Point of (TOP-REAL 2) st

( p7 = x & p7 `1 >= p7 `2 ) ;

hence x in K1 by A10; :: thesis: verum

end;then A10: ex p8 being Point of (TOP-REAL 2) st

( p8 = x & p8 `1 <= - (p8 `2) ) ;

x in K4 by A9, XBOOLE_0:def 4;

then ex p7 being Point of (TOP-REAL 2) st

( p7 = x & p7 `1 >= p7 `2 ) ;

hence x in K1 by A10; :: thesis: verum

proof

then
K1 = (K2 /\ K3) \/ (K4 /\ K5)
by A5;
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 (TOP-REAL 2) st

( p = x & ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) ) ;

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;assume x in K1 ; :: thesis: x in (K2 /\ K3) \/ (K4 /\ K5)

then ex p being Point of (TOP-REAL 2) st

( p = x & ( ( p `1 <= p `2 & - (p `2) <= p `1 ) or ( p `1 >= p `2 & p `1 <= - (p `2) ) ) ) ;

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

then A11: K1 is closed by A4, TOPS_1:9;

{ p where p is Point of (TOP-REAL 2) : ( S

then K0 = K1 /\ ([#] ((TOP-REAL 2) | B0)) by A2, PRE_TOPC:def 5;

hence ( f is continuous & K0 is closed ) by A1, A2, A3, A11, Th38, PRE_TOPC:13; :: thesis: verum