deffunc H₁( Function) -> set = *graph $1;
let Y be T_0-TopSpace; :: thesis: ( S₄[Y] implies S₃[Y] )
assume A1: S₄[Y] ; :: thesis: S₃[Y]
set T = Sigma (InclPoset the topology of Y);
let X be non empty TopSpace; :: thesis: Theta (X,Y) is isomorphic
consider G being Function such that
A2: dom G = the carrier of (ContMaps (X,(Sigma (InclPoset the topology of Y)))) and
A3: 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 object ; :: 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 object such that
A4: a in dom G and
A5: x = G . a by FUNCT_1:def 3;
reconsider a = a as Element of (ContMaps (X,(Sigma (InclPoset the topology of Y)))) by A2, A4;
reconsider a = a as continuous Function of X,(Sigma (InclPoset the topology of Y)) by WAYBEL24:21;
x = *graph a by A3, A5;
then x is open Subset of [:X,Y:] by A1;
then x in the topology of [:X,Y:] by PRE_TOPC:def 2;
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 A2, FUNCT_2:2;
consider F being Function of (InclPoset the topology of [:X,Y:]),(oContMaps (X,(Sigma (InclPoset the topology of Y)))) such that
A6: F is monotone and
A7: for W being open Subset of [:X,Y:] holds F . W = (W, the carrier of X) *graph by WAYBEL26:45;
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 Th23;
then G . f1 c= *graph f2 by A3;
then G . f1 c= G . f2 by A3;
hence G . f1 <= G . f2 by YELLOW_1:3; :: thesis: verum

end;

reconsider F = F as Function of (InclPoset the topology of [:X,Y:]),(ContMaps (X,(Sigma (InclPoset the topology of Y)))) by Th18;
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 A2, RELAT_1:27;

now :: thesis: for x being object st x in the carrier of (ContMaps (X,(Sigma (InclPoset the topology of Y)))) holds
(F * G) . x = x

let x be object ; :: 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: dom x1 = the carrier of X by FUNCT_2:def 1;

A12: now :: thesis: for i being object st i in the carrier of X holds
x1 . i = Im (gx,i)

let i be object ; :: 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 object ; :: 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:38;
hence b in Im (gx,i) by A14, RELAT_1:def 13; :: thesis: verum

end;

let b be object ; :: 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 ex j being object st
( [j,b] in gx & j in {i} ) by RELAT_1:def 13;
then [i,b] in gx by TARSKI:def 1;
hence b in x1 . i by WAYBEL26:38; :: thesis: verum

end;

end;

(F * G) . x = F . (G . x1) by A9, A10, FUNCT_1:12
.= F . gx by A3, A10
.= (gx, the carrier of X) *graph by A7 ;
hence (F * G) . x = x by A11, A12, WAYBEL26:def 5; :: thesis: verum

end;

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

now :: thesis: for x being object st x in the carrier of (InclPoset the topology of [:X,Y:]) holds
(G * F) . x = x

let x be object ; :: thesis: ( x in the carrier of (InclPoset the topology of [:X,Y:]) implies (G * F) . x = x )
assume A17: 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 2;
(x1, the carrier of X) *graph is continuous Function of X,(Sigma (InclPoset the topology of Y)) by WAYBEL26:43;
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 A18: x1 c= [: the carrier of X, the carrier of Y:] by BORSUK_1:def 2;
A19: dom x1 c= the carrier of X

proof

let d be object ; :: 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 ex e being object st [d,e] in x1 by XTUPLE_0:def 12;
hence d in the carrier of X by A18, ZFMISC_1:87; :: thesis: verum

end;

thus (G * F) . x = G . (F . x1) by A16, A17, FUNCT_1:12
.= G . x1X by A7
.= *graph x1X by A3
.= x by A19, WAYBEL26:41 ; :: thesis: verum

end;

then A20: G * F = id (InclPoset the topology of [:X,Y:]) by A16, FUNCT_1:17;
ContMaps (X,(Sigma (InclPoset the topology of Y))) = oContMaps (X,(Sigma (InclPoset the topology of Y))) by Th18;
then F is isomorphic by A6, A8, A15, A20, YELLOW16:15;
hence Theta (X,Y) is isomorphic by A7, Def3; :: thesis: verum