let X be TopSpace; :: thesis: for R being non empty SubSpace of R^1
for f, g being continuous Function of X,R
for A being Subset of X st ( for x being Point of X holds
( x in A iff f . x <= g . x ) ) holds
A is closed
let R be non empty SubSpace of R^1 ; :: thesis: for f, g being continuous Function of X,R
for A being Subset of X st ( for x being Point of X holds
( x in A iff f . x <= g . x ) ) holds
A is closed
let f, g be continuous Function of X,R; :: thesis: for A being Subset of X st ( for x being Point of X holds
( x in A iff f . x <= g . x ) ) holds
A is closed
let A be Subset of X; :: thesis: ( ( for x being Point of X holds
( x in A iff f . x <= g . x ) ) implies A is closed )
assume A1: for x being Point of X holds
( x in A iff f . x <= g . x ) ; :: thesis: A is closed

now :: thesis: ( the topology of X is Basis of X & ( 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 ` ) ) )

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

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in B or q in A ` )
reconsider qq = q as set by TARSKI:1;
assume A10: q in B ; :: thesis: q in A `
then q in g " V by XBOOLE_0:def 4;
then g . q in V by FUNCT_2:38;
then g . q in V1 by XBOOLE_0:def 4;
then A11: g . qq < (g . p) + (r / 2) by XXREAL_1:4;
q in f " U by A10, XBOOLE_0:def 4;
then f . q in U by FUNCT_2:38;
then f . q in U1 by XBOOLE_0:def 4;
then f . qq > (f . p) - (r / 2) by XXREAL_1:4;
then g . qq < f . qq by A11, XXREAL_0:2;
then not q in A by A1;
hence q in A ` by A10, SUBSET_1:29; :: thesis: verum

end;

end;

then A ` is open by YELLOW_9:31;
hence A is closed ; :: thesis: verum