defpred S1[ Point of (TOP-REAL 2)] means F1($1) <= F2($1);
reconsider K2 = { p7 where p7 is Point of (TOP-REAL 2) : S1[p7] } as Subset of (TOP-REAL 2) from JGRAPH_2:sch 1();
A3:
K2 = { p7 where p7 is Point of (TOP-REAL 2) : S1[p7] }
;
A4:
K2 ` = { p7 where p7 is Point of (TOP-REAL 2) : not S1[p7] }
from JGRAPH_2:sch 2(A3);
YY:
TopStruct(# the carrier of (TOP-REAL 2),the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2)
by EUCLID:def 8;
then reconsider K21 = K2 ` as Subset of (TopSpaceMetr (Euclid 2)) by XX;
for p being Point of (Euclid 2) st p in K21 holds
ex r being real number st
( r > 0 & Ball p,r c= K21 )
proof
let p be
Point of
(Euclid 2);
:: thesis: ( p in K21 implies ex r being real number st
( r > 0 & Ball p,r c= K21 ) )
assume A5:
p in K21
;
:: thesis: ex r being real number st
( r > 0 & Ball p,r c= K21 )
then reconsider p0 =
p as
Point of
(TOP-REAL 2) ;
set r0 =
(F1(p0) - F2(p0)) / 4;
consider p7 being
Point of
(TOP-REAL 2) such that A6:
(
p0 = p7 &
F1(
p7)
> F2(
p7) )
by A4, A5;
A7:
F1(
p0)
- F2(
p0)
> 0
by A6, XREAL_1:52;
then A8:
(F1(p0) - F2(p0)) / 4
> 0
by XREAL_1:141;
A9:
(F1(p0) - F2(p0)) / 2
> 0
by A7, XREAL_1:141;
Ball p,
((F1(p0) - F2(p0)) / 4) c= K2 `
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in Ball p,((F1(p0) - F2(p0)) / 4) or x in K2 ` )
assume A10:
x in Ball p,
((F1(p0) - F2(p0)) / 4)
;
:: thesis: x in K2 `
then reconsider px =
x as
Point of
(TOP-REAL 2) by TOPREAL3:13;
Ball p,
((F1(p0) - F2(p0)) / 4) = { q where q is Element of (Euclid 2) : dist p,q < (F1(p0) - F2(p0)) / 4 }
by METRIC_1:18;
then consider q being
Element of
(Euclid 2) such that A11:
(
q = x &
dist p,
q < (F1(p0) - F2(p0)) / 4 )
by A10;
A12:
dist p,
q = |.(p0 - px).|
by A11, JGRAPH_1:45;
A13:
|.(p0 - px).| ^2 = (F1((p0 - px)) ^2 ) + (F2((p0 - px)) ^2 )
by A2;
A14:
F2(
(p0 - px))
^2 >= 0
by XREAL_1:65;
F1(
(p0 - px))
^2 >= 0
by XREAL_1:65;
then A15:
(F2((p0 - px)) ^2 ) + 0 <= (F2((p0 - px)) ^2 ) + (F1((p0 - px)) ^2 )
by XREAL_1:9;
A16:
0 + (F1((p0 - px)) ^2 ) <= (F2((p0 - px)) ^2 ) + (F1((p0 - px)) ^2 )
by A14, XREAL_1:9;
A17:
|.(p0 - px).| ^2 <= ((F1(p0) - F2(p0)) / 4) ^2
by A11, A12, SQUARE_1:77;
then A18:
F2(
(p0 - px))
^2 <= ((F1(p0) - F2(p0)) / 4) ^2
by A13, A15, XXREAL_0:2;
A19:
F1(
(p0 - px))
^2 <= ((F1(p0) - F2(p0)) / 4) ^2
by A13, A16, A17, XXREAL_0:2;
A20:
(
F2(
(p0 - px))
= F2(
p0)
- F2(
px) &
F1(
(p0 - px))
= F1(
p0)
- F1(
px) )
by A1;
then A21:
(
- ((F1(p0) - F2(p0)) / 4) <= F2(
p0)
- F2(
px) &
F2(
p0)
- F2(
px)
<= (F1(p0) - F2(p0)) / 4 )
by A7, A18, SQUARE_1:117;
(
- ((F1(p0) - F2(p0)) / 4) <= F1(
p0)
- F1(
px) &
F1(
p0)
- F1(
px)
<= (F1(p0) - F2(p0)) / 4 )
by A7, A19, A20, SQUARE_1:117;
then
(F1(p0) - F1(px)) - (F2(p0) - F2(px)) <= ((F1(p0) - F2(p0)) / 4) - (- ((F1(p0) - F2(p0)) / 4))
by A21, XREAL_1:15;
then
F1(
px)
- F2(
px)
> 0
by A9, Lm1;
then
F1(
px)
> F2(
px)
by XREAL_1:49;
hence
x in K2 `
by A4;
:: thesis: verum
end;
hence
ex
r being
real number st
(
r > 0 &
Ball p,
r c= K21 )
by A8;
:: thesis: verum
end;
then
K21 is open
by TOPMETR:22, XX;
then
K2 ` is open
by PRE_TOPC:60, XX, YY;
hence
{ p where p is Point of (TOP-REAL 2) : F1(p) <= F2(p) } is closed Subset of (TOP-REAL 2)
by TOPS_1:29; :: thesis: verum