let T be non empty normal TopSpace; :: thesis: for A, B being closed Subset of T st A misses B holds

ex F being Function of T,R^1 st

( F is continuous & ( for x being Point of T holds

( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) )

let A, B be closed Subset of T; :: thesis: ( A misses B implies ex F being Function of T,R^1 st

( F is continuous & ( for x being Point of T holds

( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) ) )

assume A1: A misses B ; :: thesis: ex F being Function of T,R^1 st

( F is continuous & ( for x being Point of T holds

( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) )

ex F being Function of T,R^1 st

( F is continuous & ( for x being Point of T holds

( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) )

let A, B be closed Subset of T; :: thesis: ( A misses B implies ex F being Function of T,R^1 st

( F is continuous & ( for x being Point of T holds

( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) ) )

assume A1: A misses B ; :: thesis: ex F being Function of T,R^1 st

( F is continuous & ( for x being Point of T holds

( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) )

per cases
( A <> {} or A = {} )
;

end;

suppose
A <> {}
; :: thesis: ex F being Function of T,R^1 st

( F is continuous & ( for x being Point of T holds

( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) )

( F is continuous & ( for x being Point of T holds

( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) )

hence
ex F being Function of T,R^1 st

( F is continuous & ( for x being Point of T holds

( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) ) by A1, Th19; :: thesis: verum

end;( F is continuous & ( for x being Point of T holds

( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) ) by A1, Th19; :: thesis: verum

suppose A2:
A = {}
; :: thesis: ex F being Function of T,R^1 st

( F is continuous & ( for x being Point of T holds

( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) )

( F is continuous & ( for x being Point of T holds

( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) )

set S = the carrier of T;

set L = the carrier of R^1;

1 in REAL by XREAL_0:def 1;

then reconsider r = 1 as Element of the carrier of R^1 by TOPMETR:17;

defpred S_{1}[ set , set ] means $2 = r;

A3: for x being Element of the carrier of T ex y being Element of the carrier of R^1 st S_{1}[x,y]
;

ex F being Function of the carrier of T, the carrier of R^1 st

for x being Element of the carrier of T holds S_{1}[x,F . x]
from FUNCT_2:sch 3(A3);

then consider F being Function of the carrier of T, the carrier of R^1 such that

A4: for x being Element of the carrier of T holds F . x = r ;

take F ; :: thesis: ( F is continuous & ( for x being Point of T holds

( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) )

A5: dom F = the carrier of T by FUNCT_2:def 1;

thus F is continuous :: thesis: for x being Point of T holds

( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) )

thus ( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) by A2, A4; :: thesis: verum

end;set L = the carrier of R^1;

1 in REAL by XREAL_0:def 1;

then reconsider r = 1 as Element of the carrier of R^1 by TOPMETR:17;

defpred S

A3: for x being Element of the carrier of T ex y being Element of the carrier of R^1 st S

ex F being Function of the carrier of T, the carrier of R^1 st

for x being Element of the carrier of T holds S

then consider F being Function of the carrier of T, the carrier of R^1 such that

A4: for x being Element of the carrier of T holds F . x = r ;

take F ; :: thesis: ( F is continuous & ( for x being Point of T holds

( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) )

A5: dom F = the carrier of T by FUNCT_2:def 1;

thus F is continuous :: thesis: for x being Point of T holds

( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) )

proof

let x be Point of T; :: thesis: ( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) )
the carrier of T c= the carrier of T
;

then reconsider O1 = the carrier of T as Subset of T ;

reconsider O2 = {} as Subset of T by XBOOLE_1:2;

let P be Subset of R^1; :: according to PRE_TOPC:def 6 :: thesis: ( not P is closed or K433( the carrier of T, the carrier of R^1,F,P) is closed )

assume P is closed ; :: thesis: K433( the carrier of T, the carrier of R^1,F,P) is closed

A6: O2 is closed ;

end;then reconsider O1 = the carrier of T as Subset of T ;

reconsider O2 = {} as Subset of T by XBOOLE_1:2;

let P be Subset of R^1; :: according to PRE_TOPC:def 6 :: thesis: ( not P is closed or K433( the carrier of T, the carrier of R^1,F,P) is closed )

assume P is closed ; :: thesis: K433( the carrier of T, the carrier of R^1,F,P) is closed

A6: O2 is closed ;

per cases
( 1 in P or not 1 in P )
;

end;

thus ( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) by A2, A4; :: thesis: verum