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

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:46, TOPMETR:24;
reconsider U = U1 /\ ([#] R), V = V1 /\ ([#] R) as open Subset of R by TOPS_2:32;
assume A2: 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 not p in A by XBOOLE_0:def 5;
then f . p > g . p by A1;
then reconsider r = (f . p) - (g . p) as real positive number by XREAL_1:52;
take B = (f " U) /\ (g " V); :: thesis: ( B in the topology of X & p in B & B c= A ` )
( (f . p) - (r / 2) < f . p & f . p < (f . p) + (r / 2) & (g . p) - (r / 2) < g . p & g . p < (g . p) + (r / 2) ) by XREAL_1:31, XREAL_1:46;
then ( f . p in U1 & g . p in V1 & f . p in [#] R & g . p in [#] R ) by A2, FUNCT_2:7, XXREAL_1:4;
then ( f . p in U & g . p in V ) by XBOOLE_0:def 4;
then ( p in f " U & p in g " V & f " U is open & g " V is open ) by A2, FUNCT_2:46, TOPS_2:55;
then ( p in B & B is open ) by TOPS_1:38, XBOOLE_0:def 4;
hence ( B in the topology of X & p in B ) by PRE_TOPC:def 5; :: thesis: B c= A `
thus B c= A ` :: thesis: verum

proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in B or q in A ` )
assume A3: q in B ; :: thesis: q in A `
then ( q in f " U & q in g " V ) by XBOOLE_0:def 4;
then ( f . q in U & g . q in V ) by FUNCT_2:46;
then ( f . q in U1 & g . q in V1 ) by XBOOLE_0:def 4;
then ( f . q > (f . p) - (r / 2) & g . q < (g . p) + (r / 2) ) by XXREAL_1:4;
then g . q < f . q by XXREAL_0:2;
then not q in A by A1;
hence q in A ` by A3, SUBSET_1:50; :: thesis: verum

end;

end;

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