let Y be T_0-TopSpace; ( S6[Y] implies S4[Y] )
assume A1:
S6[Y]
; S4[Y]
let X be non empty TopSpace; for T being Scott TopAugmentation of InclPoset the topology of Y
for f being continuous Function of X,T holds *graph f is open Subset of [:X,Y:]
let T be Scott TopAugmentation of InclPoset the topology of Y; for f being continuous Function of X,T holds *graph f is open Subset of [:X,Y:]
let f be continuous Function of X,T; *graph f is open Subset of [:X,Y:]
( the topology of X is Basis of X & the topology of Y is Basis of Y )
by CANTOR_1:2;
then reconsider B = { [:a,b:] where a is Subset of X, b is Subset of Y : ( a in the topology of X & b in the topology of Y ) } as Basis of [:X,Y:] by YELLOW_9:40;
A2:
RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of (InclPoset the topology of Y), the InternalRel of (InclPoset the topology of Y) #)
by YELLOW_9:def 4;
now for s being object st s in *graph f holds
s in the carrier of [:X,Y:]let s be
object ;
( s in *graph f implies s in the carrier of [:X,Y:] )assume A3:
s in *graph f
;
s in the carrier of [:X,Y:]then consider s1,
s2 being
object such that A4:
s = [s1,s2]
by RELAT_1:def 1;
A5:
s1 in dom f
by A3, A4, WAYBEL26:38;
then
f . s1 in rng f
by FUNCT_1:def 3;
then
f . s1 in the
carrier of
T
;
then A6:
f . s1 in the
topology of
Y
by A2, YELLOW_1:1;
s2 in f . s1
by A3, A4, WAYBEL26:38;
then
s in [: the carrier of X, the carrier of Y:]
by A4, A5, A6, ZFMISC_1:87;
hence
s in the
carrier of
[:X,Y:]
by BORSUK_1:def 2;
verum end;
then reconsider A = *graph f as Subset of [:X,Y:] by TARSKI:def 3;
now for p being Point of [:X,Y:] st p in A holds
ex a being Subset of [:X,Y:] st
( a in B & p in a & a c= A )let p be
Point of
[:X,Y:];
( p in A implies ex a being Subset of [:X,Y:] st
( a in B & p in a & a c= A ) )assume A7:
p in A
;
ex a being Subset of [:X,Y:] st
( a in B & p in a & a c= A )then consider x,
y being
object such that A8:
p = [x,y]
by RELAT_1:def 1;
A9:
y in f . x
by A7, A8, WAYBEL26:38;
A10:
x in dom f
by A7, A8, WAYBEL26:38;
then reconsider x =
x as
Element of
X ;
f . x in the
carrier of
(InclPoset the topology of Y)
by A2;
then A11:
f . x in the
topology of
Y
by YELLOW_1:1;
then reconsider y =
y as
Element of
Y by A9;
reconsider W =
f . x as
open Subset of
Y by A11, PRE_TOPC:def 2;
y in Int W
by A9, TOPS_1:23;
then reconsider W =
W as
open a_neighborhood of
y by CONNSP_2:def 1;
consider H being
open Subset of
T such that A12:
W in H
and A13:
meet H is
a_neighborhood of
y
by A1;
[#] T <> {}
;
then reconsider fH =
f " H as
open Subset of
X by TOPS_2:43;
reconsider mH =
meet H as
a_neighborhood of
y by A13;
Int (Int mH) = Int mH
;
then reconsider V =
Int mH as
open a_neighborhood of
y by CONNSP_2:def 1;
reconsider a =
[:fH,V:] as
Subset of
[:X,Y:] ;
take a =
a;
( a in B & p in a & a c= A )
(
V in the
topology of
Y &
fH in the
topology of
X )
by PRE_TOPC:def 2;
hence
a in B
;
( p in a & a c= A )
(
y in Int mH &
x in fH )
by A10, A12, CONNSP_2:def 1, FUNCT_1:def 7;
hence
p in a
by A8, ZFMISC_1:87;
a c= Athus
a c= A
verumproof
let s1,
s2 be
object ;
RELAT_1:def 3 ( not [s1,s2] in a or [s1,s2] in A )
A14:
V c= mH
by TOPS_1:16;
assume A15:
[s1,s2] in a
;
[s1,s2] in A
then A16:
s1 in fH
by ZFMISC_1:87;
then A17:
f . s1 in H
by FUNCT_1:def 7;
A18:
s1 in dom f
by A16, FUNCT_1:def 7;
s2 in V
by A15, ZFMISC_1:87;
then
s2 in f . s1
by A17, A14, SETFAM_1:def 1;
hence
[s1,s2] in A
by A18, WAYBEL26:38;
verum
end; end;
hence
*graph f is open Subset of [:X,Y:]
by YELLOW_9:31; verum