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 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 A6: 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;
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:52;
then A8: (F1(p0) - F2(p0)) / 2 > 0 by 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 ` )
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:18;
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;
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:45;
then A13: |.(p0 - px).| ^2 <= ((F1(p0) - F2(p0)) / 4) ^2 by A12, SQUARE_1:77;
A14: F1((p0 - px)) = F1(p0) - F1(px) by A1;
A15: |.(p0 - px).| ^2 = (F1((p0 - px)) ^2 ) + (F2((p0 - px)) ^2 ) by A2;
F2((p0 - px)) ^2 >= 0 by XREAL_1:65;
then 0 + (F1((p0 - px)) ^2 ) <= (F2((p0 - px)) ^2 ) + (F1((p0 - px)) ^2 ) by XREAL_1:9;
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:117;
A17: F2((p0 - px)) = F2(p0) - F2(px) by A1;
F1((p0 - px)) ^2 >= 0 by XREAL_1:65;
then (F2((p0 - px)) ^2 ) + 0 <= (F2((p0 - px)) ^2 ) + (F1((p0 - px)) ^2 ) by XREAL_1:9;
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:117;
then (F1(p0) - F1(px)) - (F2(p0) - F2(px)) <= ((F1(p0) - F2(p0)) / 4) - (- ((F1(p0) - F2(p0)) / 4)) by A16, XREAL_1:15;
then F1(px) - F2(px) > 0 by A8, Lm2;
then F1(px) > F2(px) by XREAL_1:49;
hence x in K2 ` by A5; :: thesis: verum
end;
hence ex r being real number st
( r > 0 & Ball p,r c= K21 ) by A7, XREAL_1:141; :: thesis: verum
end;
then K21 is open by TOPMETR:22;
then K2 ` is open by A3, PRE_TOPC:60;
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