let X, Y be non empty TopSpace; :: thesis:
let S be Scott TopAugmentation of InclPoset the topology of Y; :: thesis:
let f be Function of X,S; :: thesis:
A1: RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of (InclPoset the topology of Y),the InternalRel of (InclPoset the topology of Y) #) by YELLOW_9:def 4;
A2: dom f = the carrier of X by FUNCT_2:def 1;
assume *graph f is open Subset of [:X,Y:] ; :: thesis:
then consider AA being Subset-Family of [:X,Y:] such that
A3: *graph f = union AA and
A4: for e being set st e in AA holds
ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:45;
A5: the carrier of (InclPoset the topology of Y) = the topology of Y by YELLOW_1:1;

A6: now

let P be Subset of S; :: thesis:
assume A7: P is open ; :: thesis:

now

let x be set ; :: thesis:

hereby :: thesis:

defpred S₁[ set , set ] means ( x in $2 `1 & $1 in $2 `2 & [:($2 `1 ),($2 `2 ):] c= *graph f );
assume A8: x in f " P ; :: thesis:
then reconsider y = x as Element of X ;

A9: now

let e be set ; :: thesis:
assume e in f . x ; :: thesis:
then [x,e] in *graph f by A2, A8, Th39;
then consider V being set such that
A10: [x,e] in V and
A11: V in AA by A3, TARSKI:def 4;
consider A being Subset of X, B being Subset of Y such that
A12: V = [:A,B:] and
A13: ( A is open & B is open ) by A4, A11;
reconsider u = [A,B] as set ;
take u = u; :: thesis:
( A in the topology of X & B in the topology of Y ) by A13, PRE_TOPC:def 5;
hence u in [:the topology of X,the topology of Y:] by ZFMISC_1:106; :: thesis:
( A = u `1 & B = u `2 ) by MCART_1:7;
hence S₁[e,u] by A3, A10, A11, A12, ZFMISC_1:92, ZFMISC_1:106; :: thesis:

end;

consider g being Function such that
A14: ( dom g = f . x & rng g c= [:the topology of X,the topology of Y:] ) and
A15: for a being set st a in f . x holds
S₁[a,g . a] from WELLORD2:sch 1(A9);
set J = { (union A) where A is Subset of (proj2 (rng g)) : A is finite } ;
A16: proj2 (rng g) c= the topology of Y by A14, FUNCT_5:13;
A17: { (union A) where A is Subset of (proj2 (rng g)) : A is finite } c= the topology of Y

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { (union A) where A is Subset of (proj2 (rng g)) : A is finite } ; :: thesis:
then consider A being Subset of (proj2 (rng g)) such that
A18: x = union A and
A is finite ;
A19: A c= the topology of Y by A16, XBOOLE_1:1;
then A is Subset-Family of Y by XBOOLE_1:1;
hence x in the topology of Y by A18, A19, PRE_TOPC:def 1; :: thesis:

end;

consider A0 being empty Subset of (proj2 (rng g));
A0 in { (union A) where A is Subset of (proj2 (rng g)) : A is finite } by ZFMISC_1:2;
then reconsider J = { (union A) where A is Subset of (proj2 (rng g)) : A is finite } as non empty Subset of (InclPoset the topology of Y) by A17, YELLOW_1:1;
J is directed

proof

let a, b be Element of (InclPoset the topology of Y); :: according to WAYBEL_0:def 1 :: thesis:
assume a in J ; :: thesis:
then consider A being Subset of (proj2 (rng g)) such that
A20: a = union A and
A21: A is finite ;
assume b in J ; :: thesis:
then consider B being Subset of (proj2 (rng g)) such that
A22: b = union B and
A23: B is finite ;
reconsider AB = A \/ B as finite Subset of (proj2 (rng g)) by A21, A23;
take ab = a "\/" b; :: thesis:
A24: a \/ b = ab by WAYBEL14:18;
union AB = a \/ b by A20, A22, ZFMISC_1:96;
hence ab in J by A24; :: thesis:
( a c= ab & b c= ab ) by A24, XBOOLE_1:7;
hence ( a <= ab & b <= ab ) by YELLOW_1:3; :: thesis:

end;

then reconsider J9 = J as non empty directed Subset of S by A1, WAYBEL_0:3;
A25: proj2 (rng g) c= bool (f . x)

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume z in proj2 (rng g) ; :: thesis:
then consider z1 being set such that
A26: [z1,z] in rng g by RELAT_1:def 5;
A27: [z1,z] `1 = z1 by MCART_1:7;
A28: ex a being set st
( a in dom g & [z1,z] = g . a ) by A26, FUNCT_1:def 5;
then A29: x in z1 by A14, A15, A27;
[z1,z] `2 = z by MCART_1:7;
then A30: [:z1,z:] c= *graph f by A14, A15, A28, A27;
z c= f . x

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in z ; :: thesis:
then [x,a] in [:z1,z:] by A29, ZFMISC_1:106;
hence a in f . x by A30, Th39; :: thesis:

end;

hence z in bool (f . x) ; :: thesis:

end;

union J = f . y

proof

thus union J c= f . y :: according to XBOOLE_0:def 10 :: thesis:

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in union J ; :: thesis:
then consider u being set such that
A31: a in u and
A32: u in J by TARSKI:def 4;
consider A being Subset of (proj2 (rng g)) such that
A33: u = union A and
A is finite by A32;
A c= bool (f . y) by A25, XBOOLE_1:1;
then u c= union (bool (f . y)) by A33, ZFMISC_1:95;
then u c= f . y by ZFMISC_1:99;
hence a in f . y by A31; :: thesis:

end;

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume A34: a in f . y ; :: thesis:
then A35: g . a in rng g by A14, FUNCT_1:def 5;
then g . a = [((g . a) `1 ),((g . a) `2 )] by A14, MCART_1:23;
then (g . a) `2 in proj2 (rng g) by A35, RELAT_1:def 5;
then reconsider A = {((g . a) `2 )} as Subset of (proj2 (rng g)) by ZFMISC_1:37;
union A = (g . a) `2 by ZFMISC_1:31;
then A36: (g . a) `2 in J ;
a in (g . a) `2 by A15, A34;
hence a in union J by A36, TARSKI:def 4; :: thesis:

end;

then sup J = f . y by YELLOW_1:22;
then A37: sup J9 = f . y by A1, YELLOW_0:17, YELLOW_0:26;
f . y in the topology of Y by A5, A1;
then reconsider W = f . y as open Subset of Y by PRE_TOPC:def 5;
A38: proj1 (rng g) c= the topology of X by A14, FUNCT_5:13;
defpred S₂[ set , set ] means ex c1 being set st
( [c1,$1] = g . $2 & x in c1 & $2 in $1 & $2 in f . x & [:c1,$1:] c= *graph f );
f . x in P by A8, FUNCT_2:46;
then J meets P by A7, A37, WAYBEL11:def 1;
then consider a being set such that
A39: a in J and
A40: a in P by XBOOLE_0:3;
reconsider a = a as Element of S by A40;
consider A being Subset of (proj2 (rng g)) such that
A41: a = union A and
A42: A is finite by A39;

A43: now

let c be set ; :: thesis:
assume c in A ; :: thesis:
then consider c1 being set such that
A44: [c1,c] in rng g by RELAT_1:def 5;
consider a being set such that
A45: a in dom g and
A46: [c1,c] = g . a by A44, FUNCT_1:def 5;
take a = a; :: thesis:
thus a in W by A14, A45; :: thesis:
A47: [c1,c] `1 = c1 by MCART_1:7;
then A48: x in c1 by A14, A15, A45, A46;
A49: [c1,c] `2 = c by MCART_1:7;
then [:c1,c:] c= *graph f by A14, A15, A45, A46, A47;
hence S₂[c,a] by A14, A15, A45, A46, A49, A48; :: thesis:

end;

consider hh being Function such that
A50: ( dom hh = A & rng hh c= W ) and
A51: for c being set st c in A holds
S₂[c,hh . c] from WELLORD2:sch 1(A43);
set B = proj1 (g .: (rng hh));
g .: (rng hh) c= rng g by RELAT_1:144;
then proj1 (g .: (rng hh)) c= proj1 (rng g) by FUNCT_5:5;
then A52: proj1 (g .: (rng hh)) c= the topology of X by A38, XBOOLE_1:1;
then reconsider B = proj1 (g .: (rng hh)) as Subset-Family of X by XBOOLE_1:1;
reconsider B = B as Subset-Family of X ;
reconsider Q = Intersect B as Subset of X ;
take Q = Q; :: thesis:
g .: (rng hh) is finite by A42, A50, FINSET_1:17, FINSET_1:26;
then B is finite by Th40;
then Q in FinMeetCl the topology of X by A52, CANTOR_1:def 4;
then Q in the topology of X by CANTOR_1:5;
hence Q is open by PRE_TOPC:def 5; :: thesis:
thus Q c= f " P :: thesis:

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume A53: z in Q ; :: thesis:
then reconsider zz = z as Element of X ;
reconsider fz = f . zz, aa = a as Element of (InclPoset the topology of Y) by A1;
a c= f . zz

proof

let p be set ; :: according to TARSKI:def 3 :: thesis:
assume p in a ; :: thesis:
then consider q being set such that
A54: p in q and
A55: q in A by A41, TARSKI:def 4;
consider q1 being set such that
A56: [q1,q] = g . (hh . q) and
x in q1 and
hh . q in q and
A57: hh . q in f . x and
A58: [:q1,q:] c= *graph f by A51, A55;
hh . q in rng hh by A50, A55, FUNCT_1:def 5;
then [q1,q] in g .: (rng hh) by A14, A56, A57, FUNCT_1:def 12;
then q1 in B by RELAT_1:def 4;
then zz in q1 by A53, SETFAM_1:58;
then [zz,p] in [:q1,q:] by A54, ZFMISC_1:106;
hence p in f . zz by A58, Th39; :: thesis:

end;

then aa <= fz by YELLOW_1:3;
then a <= f . zz by A1, YELLOW_0:1;
then f . zz in P by A7, A40, WAYBEL_0:def 20;
hence z in f " P by FUNCT_2:46; :: thesis:

end;

now

let c1 be set ; :: thesis:
assume c1 in B ; :: thesis:
then consider c being set such that
A59: [c1,c] in g .: (rng hh) by RELAT_1:def 4;
consider b being set such that
b in dom g and
A60: b in rng hh and
A61: [c1,c] = g . b by A59, FUNCT_1:def 12;
consider c9 being set such that
A62: c9 in dom hh and
A63: b = hh . c9 by A60, FUNCT_1:def 5;
ex c91 being set st
( [c91,c9] = g . (hh . c9) & x in c91 & hh . c9 in c9 & hh . c9 in f . x & [:c91,c9:] c= *graph f ) by A50, A51, A62;
hence x in c1 by A61, A63, ZFMISC_1:33; :: thesis:

end;

hence x in Q by A8, SETFAM_1:58; :: thesis:

end;

assume ex Q being Subset of X st
( Q is open & Q c= f " P & x in Q ) ; :: thesis:
hence x in f " P ; :: thesis:

end;

hence f " P is open by TOPS_1:57; :: thesis:

end;

[#] S <> {} ;
hence f is continuous by A6, TOPS_2:55; :: thesis: