deffunc H_{1}( Function) -> set = *graph $1;

let Y be T_0-TopSpace; :: thesis: ( S_{4}[Y] implies S_{3}[Y] )

assume A1: S_{4}[Y]
; :: thesis: S_{3}[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_{1}(f)
from FUNCT_1:sch 4();

rng G c= the carrier of (InclPoset the topology of [:X,Y:])

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

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;

A16: dom (G * F) = the carrier of (InclPoset the topology of [:X,Y:]) by FUNCT_2:def 1;

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

let Y be T_0-TopSpace; :: thesis: ( S

assume A1: S

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

rng G c= the carrier of (InclPoset the topology of [:X,Y:])

proof

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;
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;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

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

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

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

then A15:
F * G = id (ContMaps (X,(Sigma (InclPoset the topology of Y))))
by A9, FUNCT_1:17;(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;

.= 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;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)

(F * G) . x =
F . (G . x1)
by A9, A10, FUNCT_1:12
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

end;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

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;proof

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in Im (gx,i) or b in x1 . i )
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;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

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

.= 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

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

then A20:
G * F = id (InclPoset the topology of [:X,Y:])
by A16, FUNCT_1:17;(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

.= G . x1X by A7

.= *graph x1X by A3

.= x by A19, WAYBEL26:41 ; :: thesis: verum

end;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

thus (G * F) . x =
G . (F . x1)
by A16, A17, FUNCT_1:12
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;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

.= G . x1X by A7

.= *graph x1X by A3

.= x by A19, WAYBEL26:41 ; :: thesis: verum

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