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; :: thesis: 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); :: thesis: ( 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.| } ; :: thesis: 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)
proof
let p be Point of (TOP-REAL 2); :: thesis: g3 . p = (sn * |.p.|) - (p `2)
g0 . p = (2 NormF) . p by A5, Lm5
.= |.p.| by Def1 ;
then A9: g2 . p = sn * |.p.| by A1, A5;
g1 . p = proj2 . p by A5, Lm3
.= p `2 by PSCOMP_1:def 6 ;
hence g3 . p = (sn * |.p.|) - (p `2) by A3, A5, A9; :: thesis: verum
end;
A10: K1 ` c= { p7 where p7 is Point of (TOP-REAL 2) : g /. p7 > 0 }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in K1 ` or x in { p7 where p7 is Point of (TOP-REAL 2) : g /. p7 > 0 } )
assume x in K1 ` ; :: thesis: x in { p7 where p7 is Point of (TOP-REAL 2) : g /. p7 > 0 }
then consider p9 being Point of (TOP-REAL 2) such that
A11: x = p9 and
A12: p9 `2 < sn * |.p9.| by A7;
A13: g /. p9 = (sn * |.p9.|) - (p9 `2) by A8;
(sn * |.p9.|) - (p9 `2) > 0 by A12, XREAL_1:50;
hence x in { p7 where p7 is Point of (TOP-REAL 2) : g /. p7 > 0 } by A11, A13; :: thesis: verum
end;
{ p7 where p7 is Point of (TOP-REAL 2) : g /. p7 > 0 } c= K1 `
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p7 where p7 is Point of (TOP-REAL 2) : g /. p7 > 0 } or x in K1 ` )
assume x in { p7 where p7 is Point of (TOP-REAL 2) : g /. p7 > 0 } ; :: thesis: x in K1 `
then consider p7 being Point of (TOP-REAL 2) such that
A14: p7 = x and
A15: g /. p7 > 0 ;
g /. p7 = (sn * |.p7.|) - (p7 `2) by A8;
then ((sn * |.p7.|) - (p7 `2)) + (p7 `2) > 0 + (p7 `2) by A15, XREAL_1:8;
hence x in K1 ` by A7, A14; :: thesis: verum
end;
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, Th1;
then K1 ` is open by PRE_TOPC:30;
hence K1 is closed by TOPS_1:3; :: thesis: verum