set K10 = [#] (TOP-REAL 2);
reconsider g0 = (2 NormF) | ([#] (TOP-REAL 2)) as continuous Function of ((TOP-REAL 2) | ([#] (TOP-REAL 2))),R^1 by Lm5;
reconsider g1 = proj2 | ([#] (TOP-REAL 2)) as continuous Function of ((TOP-REAL 2) | ([#] (TOP-REAL 2))),R^1 by Lm3;
let sn be Real; for K1 being Subset of (TOP-REAL 2) st K1 = { p7 where p7 is Point of (TOP-REAL 2) : p7 `2 <= sn * |.p7.| } holds
K1 is closed
let K1 be Subset of (TOP-REAL 2); ( K1 = { p7 where p7 is Point of (TOP-REAL 2) : p7 `2 <= sn * |.p7.| } implies K1 is closed )
defpred S1[ Point of (TOP-REAL 2)] means $1 `2 <= sn * |.$1.|;
consider g2 being Function of ((TOP-REAL 2) | ([#] (TOP-REAL 2))),R^1 such that
A1:
for q being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2)))
for r1 being Real st g0 . q = r1 holds
g2 . q = sn * r1
and
A2:
g2 is continuous
by JGRAPH_2:23;
consider g3 being Function of ((TOP-REAL 2) | ([#] (TOP-REAL 2))),R^1 such that
A3:
for q being Point of ((TOP-REAL 2) | ([#] (TOP-REAL 2)))
for r1, r2 being Real st g2 . q = r1 & g1 . q = r2 holds
g3 . q = r1 - r2
and
A4:
g3 is continuous
by A2, JGRAPH_2:21;
A5:
(TOP-REAL 2) | ([#] (TOP-REAL 2)) = TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #)
by TSEP_1:93;
then reconsider g = g3 as Function of (TOP-REAL 2),R^1 ;
reconsider K2 = K1 as Subset of TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) ;
assume
K1 = { p where p is Point of (TOP-REAL 2) : p `2 <= sn * |.p.| }
; K1 is closed
then A6:
K1 = { p7 where p7 is Point of (TOP-REAL 2) : S1[p7] }
;
A7:
K1 ` = { p7 where p7 is Point of (TOP-REAL 2) : not S1[p7] }
from JGRAPH_2:sch 2(A6);
A8:
for p being Point of (TOP-REAL 2) holds g3 . p = (sn * |.p.|) - (p `2)
A10:
K1 ` c= { p7 where p7 is Point of (TOP-REAL 2) : g /. p7 < 0 }
{ p7 where p7 is Point of (TOP-REAL 2) : g /. p7 < 0 } c= K1 `
then
K1 ` = { p7 where p7 is Point of (TOP-REAL 2) : g /. p7 < 0 }
by A10, XBOOLE_0:def 10;
then
K2 ` is open
by A4, A5, Th2;
then
K1 ` is open
by PRE_TOPC:30;
hence
K1 is closed
by TOPS_1:3; verum