let Y be T_0-TopSpace; :: thesis: ( S_{4}[Y] implies S_{5}[Y] )

assume A1: S_{4}[Y]
; :: thesis: S_{5}[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 }

assume A1: S

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

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
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

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;proof

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 )
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;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

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