let X, Y be non empty TopSpace; :: thesis: for S being Scott TopAugmentation of InclPoset the topology of Y
for f being Function of X,S st *graph f is open Subset of [:X,Y:] holds
f is continuous

let S be Scott TopAugmentation of InclPoset the topology of Y; :: thesis: for f being Function of X,S st *graph f is open Subset of [:X,Y:] holds
f is continuous

let f be Function of X,S; :: thesis: ( *graph f is open Subset of [:X,Y:] implies f is continuous )
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: f is continuous
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:5;
A5: the carrier of (InclPoset the topology of Y) = the topology of Y by YELLOW_1:1;
A6: now :: thesis: for P being Subset of S st P is open holds
f " P is open
let P be Subset of S; :: thesis: ( P is open implies f " P is open )
assume A7: P is open ; :: thesis: f " P is open
now :: thesis: for x being set holds
( ( x in f " P implies ex Q being Subset of X st
( Q is open & Q c= f " P & x in Q ) ) & ( ex Q being Subset of X st
( Q is open & Q c= f " P & x in Q ) implies x in f " P ) )
let x be set ; :: thesis: ( ( x in f " P implies ex Q being Subset of X st
( Q is open & Q c= f " P & x in Q ) ) & ( ex Q being Subset of X st
( Q is open & Q c= f " P & x in Q ) implies x in f " P ) )

hereby :: thesis: ( ex Q being Subset of X st
( Q is open & Q c= f " P & x in Q ) implies x in f " P )
defpred S1[ object , object ] means ( x in \$2 `1 & \$1 in \$2 `2 & [:(\$2 `1),(\$2 `2):] c= *graph f );
assume A8: x in f " P ; :: thesis: ex Q being Subset of X st
( Q is open & Q c= f " P & x in Q )

then reconsider y = x as Element of X ;
A9: now :: thesis: for e being object st e in f . x holds
ex u being object st
( u in [: the topology of X, the topology of Y:] & S1[e,u] )
let e be object ; :: thesis: ( e in f . x implies ex u being object st
( u in [: the topology of X, the topology of Y:] & S1[e,u] ) )

assume e in f . x ; :: thesis: ex u being object st
( u in [: the topology of X, the topology of Y:] & S1[e,u] )

then [x,e] in *graph f by A2, A8, Th38;
then consider V being set such that
A10: [x,e] in V and
A11: V in AA by ;
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 ;
reconsider u = [A,B] as object ;
take u = u; :: thesis: ( u in [: the topology of X, the topology of Y:] & S1[e,u] )
( A in the topology of X & B in the topology of Y ) by ;
hence u in [: the topology of X, the topology of Y:] by ZFMISC_1:87; :: thesis: S1[e,u]
thus S1[e,u] by A3, A10, A11, A12, ZFMISC_1:74, ZFMISC_1:87; :: thesis: verum
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 object st a in f . x holds
S1[a,g . a] from set J = { () where A is Subset of (proj2 (rng g)) : A is finite } ;
A16: proj2 (rng g) c= the topology of Y by ;
A17: { (union A) where A is Subset of (proj2 (rng g)) : A is finite } c= the topology of Y
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { () where A is Subset of (proj2 (rng g)) : A is finite } or x in the topology of Y )
assume x in { () where A is Subset of (proj2 (rng g)) : A is finite } ; :: thesis: x in the topology of Y
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;
then A is Subset-Family of Y by XBOOLE_1:1;
hence x in the topology of Y by ; :: thesis: verum
end;
{} (proj2 (rng g)) in { () where A is Subset of (proj2 (rng g)) : A is finite } by ZFMISC_1:2;
then reconsider J = { () where A is Subset of (proj2 (rng g)) : A is finite } as non empty Subset of (InclPoset the topology of Y) by ;
J is directed
proof
let a, b be Element of (InclPoset the topology of Y); :: according to WAYBEL_0:def 1 :: thesis: ( not a in J or not b in J or ex b1 being Element of the carrier of (InclPoset the topology of Y) st
( b1 in J & a <= b1 & b <= b1 ) )

assume a in J ; :: thesis: ( not b in J or ex b1 being Element of the carrier of (InclPoset the topology of Y) st
( b1 in J & a <= b1 & b <= b1 ) )

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: ex b1 being Element of the carrier of (InclPoset the topology of Y) st
( b1 in J & a <= b1 & b <= b1 )

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 ;
take ab = a "\/" b; :: thesis: ( ab in J & a <= ab & b <= ab )
A24: a \/ b = ab by WAYBEL14:18;
union AB = a \/ b by ;
hence ab in J by A24; :: thesis: ( a <= ab & b <= ab )
( a c= ab & b c= ab ) by ;
hence ( a <= ab & b <= ab ) by YELLOW_1:3; :: thesis: verum
end;
then reconsider J9 = J as non empty directed Subset of S by ;
A25: proj2 (rng g) c= bool (f . x)
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in proj2 (rng g) or z in bool (f . x) )
reconsider zz = z as set by TARSKI:1;
assume z in proj2 (rng g) ; :: thesis: z in bool (f . x)
then consider z1 being object such that
A26: [z1,z] in rng g by XTUPLE_0:def 13;
A27: [z1,z] `1 = z1 ;
reconsider zz1 = z1 as set by TARSKI:1;
A28: ex a being object st
( a in dom g & [z1,z] = g . a ) by ;
then A29: x in zz1 by ;
[z1,z] `2 = z ;
then A30: [:zz1,zz:] c= *graph f by A14, A15, A28, A27;
zz c= f . x
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in zz or a in f . x )
assume a in zz ; :: thesis: a in f . x
then [x,a] in [:zz1,zz:] by ;
hence a in f . x by ; :: thesis: verum
end;
hence z in bool (f . x) ; :: thesis: verum
end;
union J = f . y
proof
thus union J c= f . y :: according to XBOOLE_0:def 10 :: thesis: f . y c= union J
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in union J or a in f . y )
assume a in union J ; :: thesis: a in f . y
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;
then u c= union (bool (f . y)) by ;
then u c= f . y by ZFMISC_1:81;
hence a in f . y by A31; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in f . y or a in union J )
assume A34: a in f . y ; :: thesis: a in union J
then A35: g . a in rng g by ;
then g . a = [((g . a) `1),((g . a) `2)] by ;
then (g . a) `2 in proj2 (rng g) by ;
then reconsider A = {((g . a) `2)} as Subset of (proj2 (rng g)) by ZFMISC_1:31;
union A = (g . a) `2 by ZFMISC_1:25;
then A36: (g . a) `2 in J ;
a in (g . a) `2 by ;
hence a in union J by ; :: thesis: verum
end;
then sup J = f . y by YELLOW_1:22;
then A37: sup J9 = f . y by ;
f . y in the topology of Y by A5, A1;
then reconsider W = f . y as open Subset of Y by PRE_TOPC:def 2;
A38: proj1 (rng g) c= the topology of X by ;
defpred S2[ object , object ] means ex c1, d being set st
( d = \$1 & [c1,\$1] = g . \$2 & x in c1 & \$2 in d & \$2 in f . x & [:c1,d:] c= *graph f );
f . x in P by ;
then J meets P by ;
then consider a being object 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 :: thesis: for c being object st c in A holds
ex a being object st
( a in W & S2[c,a] )
let c be object ; :: thesis: ( c in A implies ex a being object st
( a in W & S2[c,a] ) )

assume c in A ; :: thesis: ex a being object st
( a in W & S2[c,a] )

then consider c1 being object such that
A44: [c1,c] in rng g by XTUPLE_0:def 13;
reconsider cc1 = c1 as set by TARSKI:1;
consider a being object such that
A45: a in dom g and
A46: [c1,c] = g . a by ;
reconsider cc = c as set by TARSKI:1;
reconsider a = a as object ;
take a = a; :: thesis: ( a in W & S2[c,a] )
thus a in W by ; :: thesis: S2[c,a]
A47: [c1,c] `1 = c1 ;
then A48: x in cc1 by A14, A15, A45, A46;
A49: [c1,c] `2 = c ;
then [:cc1,cc:] c= *graph f by A14, A15, A45, A46, A47;
hence S2[c,a] by A14, A15, A45, A46, A49, A48; :: thesis: verum
end;
consider hh being Function such that
A50: ( dom hh = A & rng hh c= W ) and
A51: for c being object st c in A holds
S2[c,hh . c] from set B = proj1 (g .: (rng hh));
g .: (rng hh) c= rng g by RELAT_1:111;
then proj1 (g .: (rng hh)) c= proj1 (rng g) by XTUPLE_0:8;
then A52: proj1 (g .: (rng hh)) c= the topology of X by A38;
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: ( Q is open & Q c= f " P & x in Q )
g .: (rng hh) is finite by ;
then B is finite by Th39;
then Q in FinMeetCl the topology of X by ;
then Q in the topology of X by CANTOR_1:5;
hence Q is open by PRE_TOPC:def 2; :: thesis: ( Q c= f " P & x in Q )
thus Q c= f " P :: thesis: x in Q
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Q or z in f " P )
assume A53: z in Q ; :: thesis: z in f " P
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 object ; :: according to TARSKI:def 3 :: thesis: ( not p in a or p in f . zz )
assume p in a ; :: thesis: p in f . zz
then consider q being set such that
A54: p in q and
A55: q in A by ;
S2[q,hh . q] by ;
then consider q1, d being set such that
A56: d = q and
A57: [q1,q] = g . (hh . q) and
A58: hh . q in f . x and
A59: [:q1,d:] c= *graph f ;
hh . q in rng hh by ;
then [q1,q] in g .: (rng hh) by ;
then q1 in B by XTUPLE_0:def 12;
then zz in q1 by ;
then [zz,p] in [:q1,q:] by ;
hence p in f . zz by ; :: thesis: verum
end;
then aa <= fz by YELLOW_1:3;
then a <= f . zz by ;
then f . zz in P by ;
hence z in f " P by FUNCT_2:38; :: thesis: verum
end;
now :: thesis: for c1 being set st c1 in B holds
x in c1
let c1 be set ; :: thesis: ( c1 in B implies x in c1 )
assume c1 in B ; :: thesis: x in c1
then consider c being object such that
A60: [c1,c] in g .: (rng hh) by XTUPLE_0:def 12;
consider b being object such that
b in dom g and
A61: b in rng hh and
A62: [c1,c] = g . b by ;
consider c9 being object such that
A63: c9 in dom hh and
A64: b = hh . c9 by ;
ex c91, d being set st
( d = c9 & [c91,c9] = g . (hh . c9) & x in c91 & hh . c9 in d & hh . c9 in f . x & [:c91,d:] c= *graph f ) by ;
hence x in c1 by ; :: thesis: verum
end;
hence x in Q by ; :: thesis: verum
end;
assume ex Q being Subset of X st
( Q is open & Q c= f " P & x in Q ) ; :: thesis: x in f " P
hence x in f " P ; :: thesis: verum
end;
hence f " P is open by TOPS_1:25; :: thesis: verum
end;
[#] S <> {} ;
hence f is continuous by ; :: thesis: verum