let Y be T_0-TopSpace; :: thesis: ( S6[Y] implies S4[Y] )
assume A1:
S6[Y]
; :: thesis: S4[Y]
let X be non empty TopSpace; :: thesis: 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; :: thesis: 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; :: thesis: *graph f is open Subset of [:X,Y:]
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;
( 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;
now let s be
set ;
:: thesis: ( s in *graph f implies s in the carrier of [:X,Y:] )assume A3:
s in *graph f
;
:: thesis: s in the carrier of [:X,Y:]then consider s1,
s2 being
set such that A4:
s = [s1,s2]
by RELAT_1:def 1;
A5:
(
s1 in dom f &
s2 in f . s1 )
by A3, A4, WAYBEL26:39;
then
f . s1 in rng f
by FUNCT_1:def 5;
then
f . s1 in the
carrier of
T
;
then
f . s1 in the
topology of
Y
by A2, YELLOW_1:1;
then
s in [:the carrier of X,the carrier of Y:]
by A4, A5, ZFMISC_1:106;
hence
s in the
carrier of
[:X,Y:]
by BORSUK_1:def 5;
:: thesis: verum end;
then reconsider A = *graph f as Subset of [:X,Y:] by TARSKI:def 3;
now let p be
Point of
[:X,Y:];
:: thesis: ( p in A implies ex a being Subset of [:X,Y:] st
( a in B & p in a & a c= A ) )assume A6:
p in A
;
:: thesis: ex a being Subset of [:X,Y:] st
( a in B & p in a & a c= A )then consider x,
y being
set such that A7:
p = [x,y]
by RELAT_1:def 1;
A8:
(
x in dom f &
y in f . x )
by A6, A7, WAYBEL26:39;
then reconsider x =
x as
Element of
X ;
f . x in the
carrier of
(InclPoset the topology of Y)
by A2;
then A9:
f . x in the
topology of
Y
by YELLOW_1:1;
then reconsider y =
y as
Element of
Y by A8;
reconsider W =
f . x as
open Subset of
Y by A9, PRE_TOPC:def 5;
y in Int W
by A8, TOPS_1:55;
then reconsider W =
W as
open a_neighborhood of
y by CONNSP_2:def 1;
consider H being
open Subset of
T such that A10:
(
W in H &
meet H is
a_neighborhood of
y )
by A1;
reconsider mH =
meet H as
a_neighborhood of
y by A10;
A11:
(
y in Int mH &
Int (Int mH) = Int mH )
by CONNSP_2:def 1;
then reconsider V =
Int mH as
open a_neighborhood of
y by CONNSP_2:def 1;
[#] T <> {}
;
then reconsider fH =
f " H as
open Subset of
X by TOPS_2:55;
reconsider a =
[:fH,V:] as
Subset of
[:X,Y:] ;
take a =
a;
:: thesis: ( 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 5;
hence
a in B
;
:: thesis: ( p in a & a c= A )
x in fH
by A8, A10, FUNCT_1:def 13;
hence
p in a
by A7, A11, ZFMISC_1:106;
:: thesis: a c= Athus
a c= A
:: thesis: verumproof
let s1,
s2 be
set ;
:: according to RELAT_1:def 3 :: thesis: ( not [s1,s2] in a or [s1,s2] in A )
assume
[s1,s2] in a
;
:: thesis: [s1,s2] in A
then A12:
(
s1 in fH &
s2 in V )
by ZFMISC_1:106;
then A13:
f . s1 in H
by FUNCT_1:def 13;
V c= mH
by TOPS_1:44;
then A14:
s2 in f . s1
by A12, A13, SETFAM_1:def 1;
s1 in dom f
by A12, FUNCT_1:def 13;
hence
[s1,s2] in A
by A14, WAYBEL26:39;
:: thesis: verum
end; end;
hence
*graph f is open Subset of [:X,Y:]
by YELLOW_9:31; :: thesis: verum