let Y be T_0-TopSpace; :: thesis: ( S4[Y] implies S5[Y] )
assume A1:
S4[Y]
; :: thesis: S5[Y]
let X be Scott TopAugmentation of InclPoset the topology of Y; :: thesis: { [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 }
:: according to XBOOLE_0:def 10 :: thesis: { [W,y] where W is open Subset of Y, y is Element of Y : y in W } c= *graph fproof
let a,
b be
set ;
:: according to RELAT_1:def 3 :: thesis: ( 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
[a,b] in *graph f
;
:: thesis: [a,b] in { [W,y] where W is open Subset of Y, y is Element of Y : y in W }
then A3:
(
a in dom f &
b in f . a )
by WAYBEL26:39;
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 A3, PRE_TOPC:def 5;
f . a = a
by A3, FUNCT_1:35;
then reconsider b =
b as
Element of
Y by A3;
b in a
by A3, FUNCT_1:35;
hence
[a,b] in { [W,y] where W is open Subset of Y, y is Element of Y : y in W }
;
:: thesis: verum
end;
let e be
set ;
:: according to TARSKI:def 3 :: thesis: ( 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 }
;
:: thesis: e in *graph f
then consider W being
open Subset of
Y,
y being
Element of
Y such that A4:
(
e = [W,y] &
y in W )
;
W in the
topology of
Y
by PRE_TOPC:def 5;
then A5:
W in the
carrier of
(InclPoset the topology of Y)
by YELLOW_1:1;
then A6:
W in dom f
by A2, FUNCT_2:def 1;
f . W = W
by A2, A5, FUNCT_1:35;
hence
e in *graph f
by A4, A6, WAYBEL26:39;
:: thesis: 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; :: thesis: verum