let Y be T_0-TopSpace; ( S4[Y] implies S5[Y] )
assume A1:
S4[Y]
; S5[Y]
let X be Scott TopAugmentation of InclPoset the topology of Y; { [W,y] where W is open Subset of Y, y is Element of Y : y in W } is open Subset of [:X,Y:]
reconsider f = id X as continuous Function of X,X ;
A2:
RelStr(# the carrier of X, the InternalRel of X #) = RelStr(# the carrier of (InclPoset the topology of Y), the InternalRel of (InclPoset the topology of Y) #)
by YELLOW_9:def 4;
*graph f = { [W,y] where W is open Subset of Y, y is Element of Y : y in W }
proof
thus
*graph f c= { [W,y] where W is open Subset of Y, y is Element of Y : y in W }
XBOOLE_0:def 10 { [W,y] where W is open Subset of Y, y is Element of Y : y in W } c= *graph fproof
let a,
b be
object ;
RELAT_1:def 3 ( not [a,b] in *graph f or [a,b] in { [W,y] where W is open Subset of Y, y is Element of Y : y in W } )
assume A3:
[a,b] in *graph f
;
[a,b] in { [W,y] where W is open Subset of Y, y is Element of Y : y in W }
then A4:
a in dom f
by WAYBEL26:38;
A5:
b in f . a
by A3, WAYBEL26:38;
dom f =
the
carrier of
(InclPoset the topology of Y)
by A2, FUNCT_2:def 1
.=
the
topology of
Y
by YELLOW_1:1
;
then reconsider a =
a as
open Subset of
Y by A4, PRE_TOPC:def 2;
f . a = a
by A4, FUNCT_1:18;
then reconsider b =
b as
Element of
Y by A5;
b in a
by A4, A5, FUNCT_1:18;
hence
[a,b] in { [W,y] where W is open Subset of Y, y is Element of Y : y in W }
;
verum
end;
let e be
object ;
TARSKI:def 3 ( not e in { [W,y] where W is open Subset of Y, y is Element of Y : y in W } or e in *graph f )
assume
e in { [W,y] where W is open Subset of Y, y is Element of Y : y in W }
;
e in *graph f
then consider W being
open Subset of
Y,
y being
Element of
Y such that A6:
(
e = [W,y] &
y in W )
;
W in the
topology of
Y
by PRE_TOPC:def 2;
then
W in the
carrier of
(InclPoset the topology of Y)
by YELLOW_1:1;
then
(
W in dom f &
f . W = W )
by A2, FUNCT_1:18, FUNCT_2:def 1;
hence
e in *graph f
by A6, WAYBEL26:38;
verum
end;
hence
{ [W,y] where W is open Subset of Y, y is Element of Y : y in W } is open Subset of [:X,Y:]
by A1; verum