let Y be T_0-TopSpace; :: thesis: ( S₄[Y] implies S₅[Y] )
assume A1: S₄[Y] ; :: thesis: S₅[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 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 } ; :: 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 A2, FUNCT_1:18, FUNCT_2:def 1;
hence e in *graph f by A6, WAYBEL26:38; :: 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