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 f
proof
let a, b be object ; :: 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 A3: [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 A4: a in dom f by WAYBEL26:38;
A5: b in f . a by ;
dom f = the carrier of (InclPoset the topology of Y) by
.= the topology of Y by YELLOW_1:1 ;
then reconsider a = a as open Subset of Y by ;
f . a = a by ;
then reconsider b = b as Element of Y by A5;
b in a by ;
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 object ; :: 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
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 ;
hence e in *graph f by ; :: 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