let Y be T_0-TopSpace; :: thesis: ( S₄[Y] implies S₃[Y] )
assume A1: S₄[Y] ; :: thesis: S₃[Y]
let X be non empty TopSpace; :: thesis: Theta X,Y is isomorphic
set T = Sigma (InclPoset the topology of Y);
consider F being Function of (InclPoset the topology of [:X,Y:]),(oContMaps X,(Sigma (InclPoset the topology of Y))) such that
A2: F is monotone and
A3: for W being open Subset of [:X,Y:] holds F . W = W,the carrier of X *graph by WAYBEL26:46;
A4: ContMaps X,(Sigma (InclPoset the topology of Y)) = oContMaps X,(Sigma (InclPoset the topology of Y)) by Th22;
then reconsider F = F as Function of (InclPoset the topology of [:X,Y:]),(ContMaps X,(Sigma (InclPoset the topology of Y))) ;
deffunc H₁( Function) -> set = *graph $1;
consider G being Function such that
A5: dom G = the carrier of (ContMaps X,(Sigma (InclPoset the topology of Y))) and
A6: for f being Element of (ContMaps X,(Sigma (InclPoset the topology of Y))) holds G . f = H₁(f) from FUNCT_1:sch 4();
rng G c= the carrier of (InclPoset the topology of [:X,Y:])

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng G or x in the carrier of (InclPoset the topology of [:X,Y:]) )
assume x in rng G ; :: thesis: x in the carrier of (InclPoset the topology of [:X,Y:])
then consider a being set such that
A7: ( a in dom G & x = G . a ) by FUNCT_1:def 5;
reconsider a = a as Element of (ContMaps X,(Sigma (InclPoset the topology of Y))) by A5, A7;
reconsider a = a as continuous Function of X,(Sigma (InclPoset the topology of Y)) by WAYBEL24:21;
x = *graph a by A6, A7;
then x is open Subset of [:X,Y:] by A1;
then x in the topology of [:X,Y:] by PRE_TOPC:def 5;
hence x in the carrier of (InclPoset the topology of [:X,Y:]) by YELLOW_1:1; :: thesis: verum

end;

then reconsider G = G as Function of (ContMaps X,(Sigma (InclPoset the topology of Y))),(InclPoset the topology of [:X,Y:]) by A5, FUNCT_2:4;
A8: G is monotone

proof

let f1, f2 be Element of (ContMaps X,(Sigma (InclPoset the topology of Y))); :: according to WAYBEL_1:def 2 :: thesis: ( not f1 <= f2 or G . f1 <= G . f2 )
assume f1 <= f2 ; :: thesis: G . f1 <= G . f2
then *graph f1 c= *graph f2 by Th27;
then G . f1 c= *graph f2 by A6;
then G . f1 c= G . f2 by A6;
hence G . f1 <= G . f2 by YELLOW_1:3; :: thesis: verum

end;

dom F = the carrier of (InclPoset the topology of [:X,Y:]) by FUNCT_2:def 1;
then rng G c= dom F ;
then A9: dom (F * G) = the carrier of (ContMaps X,(Sigma (InclPoset the topology of Y))) by A5, RELAT_1:46;

now

let x be set ; :: thesis: ( x in the carrier of (ContMaps X,(Sigma (InclPoset the topology of Y))) implies (F * G) . x = x )
assume A10: x in the carrier of (ContMaps X,(Sigma (InclPoset the topology of Y))) ; :: thesis: (F * G) . x = x
then reconsider x1 = x as continuous Function of X,(Sigma (InclPoset the topology of Y)) by WAYBEL24:21;
reconsider gx = *graph x1 as open Subset of [:X,Y:] by A1;
A11: (F * G) . x = F . (G . x1) by A9, A10, FUNCT_1:22
.= F . gx by A6, A10
.= gx,the carrier of X *graph by A3 ;
A12: dom x1 = the carrier of X by FUNCT_2:def 1;

now

let i be set ; :: thesis: ( i in the carrier of X implies x1 . i = Im gx,i )
assume i in the carrier of X ; :: thesis: x1 . i = Im gx,i
then A13: i in dom x1 by FUNCT_2:def 1;
A14: i in {i} by TARSKI:def 1;
thus x1 . i = Im gx,i :: thesis: verum

proof

thus x1 . i c= Im gx,i :: according to XBOOLE_0:def 10 :: thesis: Im gx,i c= x1 . i

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in x1 . i or b in Im gx,i )
assume b in x1 . i ; :: thesis: b in Im gx,i
then [i,b] in gx by A13, WAYBEL26:39;
hence b in Im gx,i by A14, RELAT_1:def 13; :: thesis: verum

end;

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in Im gx,i or b in x1 . i )
assume b in Im gx,i ; :: thesis: b in x1 . i
then consider j being set such that
A15: ( [j,b] in gx & j in {i} ) by RELAT_1:def 13;
[i,b] in gx by A15, TARSKI:def 1;
hence b in x1 . i by WAYBEL26:39; :: thesis: verum

end;

end;

hence (F * G) . x = x by A11, A12, WAYBEL26:def 5; :: thesis: verum

end;

then A16: F * G = id (ContMaps X,(Sigma (InclPoset the topology of Y))) by A9, FUNCT_1:34;
A17: dom (G * F) = the carrier of (InclPoset the topology of [:X,Y:]) by FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in the carrier of (InclPoset the topology of [:X,Y:]) implies (G * F) . x = x )
assume A18: x in the carrier of (InclPoset the topology of [:X,Y:]) ; :: thesis: (G * F) . x = x
then x in the topology of [:X,Y:] by YELLOW_1:1;
then reconsider x1 = x as open Subset of [:X,Y:] by PRE_TOPC:def 5;
x1,the carrier of X *graph is continuous Function of X,(Sigma (InclPoset the topology of Y)) by WAYBEL26:44;
then reconsider x1X = x1,the carrier of X *graph as Element of (ContMaps X,(Sigma (InclPoset the topology of Y))) by WAYBEL24:21;
x1 c= the carrier of [:X,Y:] ;
then A19: x1 c= [:the carrier of X,the carrier of Y:] by BORSUK_1:def 5;
A20: dom x1 c= the carrier of X

proof

let d be set ; :: according to TARSKI:def 3 :: thesis: ( not d in dom x1 or d in the carrier of X )
assume d in dom x1 ; :: thesis: d in the carrier of X
then consider e being set such that
A21: [d,e] in x1 by RELAT_1:def 4;
thus d in the carrier of X by A19, A21, ZFMISC_1:106; :: thesis: verum

end;

thus (G * F) . x = G . (F . x1) by A17, A18, FUNCT_1:22
.= G . x1X by A3
.= *graph x1X by A6
.= x by A20, WAYBEL26:42 ; :: thesis: verum

end;

then G * F = id (InclPoset the topology of [:X,Y:]) by A17, FUNCT_1:34;
then F is isomorphic by A2, A4, A8, A16, YELLOW16:17;
hence Theta X,Y is isomorphic by A3, Def3; :: thesis: verum