thus the topology of X is Basis of X by CANTOR_1:2; :: thesis: for p being Point of X st p in A ` holds
ex B being Element of bool the carrier of X st
( B in the topology of X & p in B & B c= A ` )
let p be Point of X; :: thesis: ( p in A ` implies ex B being Element of bool the carrier of X st
( B in the topology of X & p in B & B c= A ` ) )
set r = (f . p) - (g . p);
reconsider U1 = ].((f . p) - (((f . p) - (g . p)) / 2)),((f . p) + (((f . p) - (g . p)) / 2)).[, V1 = ].((g . p) - (((f . p) - (g . p)) / 2)),((g . p) + (((f . p) - (g . p)) / 2)).[ as open Subset of R^1 by JORDAN6:35, TOPMETR:17;
reconsider U = U1 /\ ([#] R), V = V1 /\ ([#] R) as open Subset of R by TOPS_2:24;
A2: g " V is open by TOPS_2:43;
assume A3: p in A ` ; :: thesis: ex B being Element of bool the carrier of X st
( B in the topology of X & p in B & B c= A ` )
then A4: f . p in [#] R by FUNCT_2:5;
not p in A by A3, XBOOLE_0:def 5;
then f . p > g . p by A1;
then reconsider r = (f . p) - (g . p) as positive Real by XREAL_1:50;
A5: f . p < (f . p) + (r / 2) by XREAL_1:29;
take B = (f " U) /\ (g " V); :: thesis: ( B in the topology of X & p in B & B c= A ` )
A6: g . p < (g . p) + (r / 2) by XREAL_1:29;
A7: g . p in [#] R by A3, FUNCT_2:5;
(g . p) - (r / 2) < g . p by XREAL_1:44;
then g . p in V1 by A6, XXREAL_1:4;
then g . p in V by A7, XBOOLE_0:def 4;
then A8: p in g " V by A3, FUNCT_2:38;
(f . p) - (r / 2) < f . p by XREAL_1:44;
then f . p in U1 by A5, XXREAL_1:4;
then f . p in U by A4, XBOOLE_0:def 4;
then A9: p in f " U by A3, FUNCT_2:38;
f " U is open by TOPS_2:43;
hence ( B in the topology of X & p in B ) by A9, A8, A2, PRE_TOPC:def 2, XBOOLE_0:def 4; :: thesis: B c= A `
thus B c= A ` :: thesis: verum