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: 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)) ;
A4: K2 = { p7 where p7 is Point of (TOP-REAL 2) : S1[p7] } ;
A5: K2 ` = { p7 where p7 is Point of (TOP-REAL 2) : not S1[p7] } from JGRAPH_2:sch 2(A4);
 for p being Point of (Euclid 2) st p in K21 holds
ex r being Real 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 st
( r > 0 & Ball (p,r) c= K21 ) )
assume A6: p in K21 ; :: thesis: ex r being Real 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;
ex p7 being Point of (TOP-REAL 2) st
( p0 = p7 & F1(p7) > F2(p7) ) by A5, A6;
then A7: F1(p0) - F2(p0) > 0 by XREAL_1:50;
then A8: (F1(p0) - F2(p0)) / 2 > 0 by XREAL_1:139;
Ball (p,((F1(p0) - F2(p0)) / 4)) c= K2 `
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Ball (p,((F1(p0) - F2(p0)) / 4)) or x in K2 ` )
A9: 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:17;
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:8;
consider q being Element of (Euclid 2) such that
A11: q = x and
A12: dist (p,q) < (F1(p0) - F2(p0)) / 4 by A10, A9;
dist (p,q) = |.(p0 - px).| by A11, JGRAPH_1:28;
then A13: |.(p0 - px).| ^2 <= ((F1(p0) - F2(p0)) / 4) ^2 by A12, SQUARE_1:15;
A14: F1((p0 - px)) = F1(p0) - F1(px) by A1;
A15: |.(p0 - px).| ^2 = (F1((p0 - px)) ^2) + (F2((p0 - px)) ^2) by A2;
0 + (F1((p0 - px)) ^2) <= (F2((p0 - px)) ^2) + (F1((p0 - px)) ^2) by XREAL_1:7;
then F1((p0 - px)) ^2 <= ((F1(p0) - F2(p0)) / 4) ^2 by A15, A13, XXREAL_0:2;
then A16: F1(p0) - F1(px) <= (F1(p0) - F2(p0)) / 4 by A7, A14, SQUARE_1:47;
A17: F2((p0 - px)) = F2(p0) - F2(px) by A1;
(F2((p0 - px)) ^2) + 0 <= (F2((p0 - px)) ^2) + (F1((p0 - px)) ^2) by XREAL_1:7;
then F2((p0 - px)) ^2 <= ((F1(p0) - F2(p0)) / 4) ^2 by A15, A13, XXREAL_0:2;
then - ((F1(p0) - F2(p0)) / 4) <= F2(p0) - F2(px) by A7, A17, SQUARE_1:47;
then (F1(p0) - F1(px)) - (F2(p0) - F2(px)) <= ((F1(p0) - F2(p0)) / 4) - (- ((F1(p0) - F2(p0)) / 4)) by A16, XREAL_1:13;
then F1(px) - F2(px) > 0 by A8, Lm2;
then F1(px) > F2(px) by XREAL_1:47;
hence x in K2 ` by A5; :: thesis: verum
end;
hence ex r being Real st
( r > 0 & Ball (p,r) c= K21 ) by A7, XREAL_1:139; :: thesis: verum
end;
then K21 is open by TOPMETR:15;
then K2 ` is open by A3, PRE_TOPC:30;
hence { p where p is Point of (TOP-REAL 2) : F1(p) <= F2(p) } is closed Subset of (TOP-REAL 2) by TOPS_1:3; :: thesis: verum