let Y be T_0-TopSpace; :: thesis: ( S_{6}[Y] implies InclPoset the topology of Y is continuous )

assume A1: S_{6}[Y]
; :: thesis: InclPoset the topology of Y is continuous

set L = InclPoset the topology of Y;

set S = the Scott TopAugmentation of InclPoset the topology of Y;

thus for x being Element of (InclPoset the topology of Y) holds

( not waybelow x is empty & waybelow x is directed ) ; :: according to WAYBEL_3:def 6 :: thesis: ( InclPoset the topology of Y is up-complete & InclPoset the topology of Y is satisfying_axiom_of_approximation )

thus InclPoset the topology of Y is up-complete ; :: thesis: InclPoset the topology of Y is satisfying_axiom_of_approximation

let A be Element of (InclPoset the topology of Y); :: according to WAYBEL_3:def 5 :: thesis: A = "\/" ((waybelow A),(InclPoset the topology of Y))

the carrier of (InclPoset the topology of Y) = the topology of Y by YELLOW_1:1;

then A in the topology of Y ;

then reconsider B = A as open Subset of Y by PRE_TOPC:def 2;

A2: RelStr(# the carrier of the Scott TopAugmentation of InclPoset the topology of Y, the InternalRel of the Scott TopAugmentation of InclPoset the topology of Y #) = RelStr(# the carrier of (InclPoset the topology of Y), the InternalRel of (InclPoset the topology of Y) #) by YELLOW_9:def 4;

thus A c= sup (waybelow A) :: according to XBOOLE_0:def 10 :: thesis: "\/" ((waybelow A),(InclPoset the topology of Y)) c= A

then sup (waybelow A) c= union (downarrow A) by YELLOW_1:22;

then sup (waybelow A) c= sup (downarrow A) by YELLOW_1:22;

hence "\/" ((waybelow A),(InclPoset the topology of Y)) c= A by WAYBEL_0:34; :: thesis: verum

assume A1: S

set L = InclPoset the topology of Y;

set S = the Scott TopAugmentation of InclPoset the topology of Y;

thus for x being Element of (InclPoset the topology of Y) holds

( not waybelow x is empty & waybelow x is directed ) ; :: according to WAYBEL_3:def 6 :: thesis: ( InclPoset the topology of Y is up-complete & InclPoset the topology of Y is satisfying_axiom_of_approximation )

thus InclPoset the topology of Y is up-complete ; :: thesis: InclPoset the topology of Y is satisfying_axiom_of_approximation

let A be Element of (InclPoset the topology of Y); :: according to WAYBEL_3:def 5 :: thesis: A = "\/" ((waybelow A),(InclPoset the topology of Y))

the carrier of (InclPoset the topology of Y) = the topology of Y by YELLOW_1:1;

then A in the topology of Y ;

then reconsider B = A as open Subset of Y by PRE_TOPC:def 2;

A2: RelStr(# the carrier of the Scott TopAugmentation of InclPoset the topology of Y, the InternalRel of the Scott TopAugmentation of InclPoset the topology of Y #) = RelStr(# the carrier of (InclPoset the topology of Y), the InternalRel of (InclPoset the topology of Y) #) by YELLOW_9:def 4;

thus A c= sup (waybelow A) :: according to XBOOLE_0:def 10 :: thesis: "\/" ((waybelow A),(InclPoset the topology of Y)) c= A

proof

union (waybelow A) c= union (downarrow A)
by WAYBEL_3:11, ZFMISC_1:77;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in sup (waybelow A) )

assume A3: x in A ; :: thesis: x in sup (waybelow A)

then x in B ;

then reconsider x9 = x as Element of Y ;

reconsider B = B as open a_neighborhood of x9 by A3, CONNSP_2:3;

consider H being open Subset of the Scott TopAugmentation of InclPoset the topology of Y such that

A4: B in H and

A5: meet H is a_neighborhood of x9 by A1;

reconsider mH = meet H as a_neighborhood of x9 by A5;

reconsider H1 = H as Subset of (InclPoset the topology of Y) by A2;

Int mH in the topology of Y by PRE_TOPC:def 2;

then reconsider ImH = Int mH as Element of (InclPoset the topology of Y) by YELLOW_1:1;

ImH << A

then x in union (waybelow A) by TARSKI:def 4;

hence x in sup (waybelow A) by YELLOW_1:22; :: thesis: verum

end;assume A3: x in A ; :: thesis: x in sup (waybelow A)

then x in B ;

then reconsider x9 = x as Element of Y ;

reconsider B = B as open a_neighborhood of x9 by A3, CONNSP_2:3;

consider H being open Subset of the Scott TopAugmentation of InclPoset the topology of Y such that

A4: B in H and

A5: meet H is a_neighborhood of x9 by A1;

reconsider mH = meet H as a_neighborhood of x9 by A5;

reconsider H1 = H as Subset of (InclPoset the topology of Y) by A2;

Int mH in the topology of Y by PRE_TOPC:def 2;

then reconsider ImH = Int mH as Element of (InclPoset the topology of Y) by YELLOW_1:1;

ImH << A

proof

then
( x in Int mH & Int mH in waybelow A )
by CONNSP_2:def 1;
let D be non empty directed Subset of (InclPoset the topology of Y); :: according to WAYBEL_3:def 1 :: thesis: ( not A <= "\/" (D,(InclPoset the topology of Y)) or ex b_{1} being Element of the carrier of (InclPoset the topology of Y) st

( b_{1} in D & ImH <= b_{1} ) )

A6: ( H1 is inaccessible & H1 is upper ) by A2, WAYBEL_0:25, YELLOW_9:47;

assume A <= sup D ; :: thesis: ex b_{1} being Element of the carrier of (InclPoset the topology of Y) st

( b_{1} in D & ImH <= b_{1} )

then sup D in H1 by A4, A6;

then D meets H1 by A6;

then consider d being object such that

A7: d in D and

A8: d in H1 by XBOOLE_0:3;

reconsider d = d as Element of (InclPoset the topology of Y) by A7;

take d ; :: thesis: ( d in D & ImH <= d )

thus d in D by A7; :: thesis: ImH <= d

( Int mH c= mH & mH c= d ) by A8, SETFAM_1:3, TOPS_1:16;

then ImH c= d ;

hence ImH <= d by YELLOW_1:3; :: thesis: verum

end;( b

A6: ( H1 is inaccessible & H1 is upper ) by A2, WAYBEL_0:25, YELLOW_9:47;

assume A <= sup D ; :: thesis: ex b

( b

then sup D in H1 by A4, A6;

then D meets H1 by A6;

then consider d being object such that

A7: d in D and

A8: d in H1 by XBOOLE_0:3;

reconsider d = d as Element of (InclPoset the topology of Y) by A7;

take d ; :: thesis: ( d in D & ImH <= d )

thus d in D by A7; :: thesis: ImH <= d

( Int mH c= mH & mH c= d ) by A8, SETFAM_1:3, TOPS_1:16;

then ImH c= d ;

hence ImH <= d by YELLOW_1:3; :: thesis: verum

then x in union (waybelow A) by TARSKI:def 4;

hence x in sup (waybelow A) by YELLOW_1:22; :: thesis: verum

then sup (waybelow A) c= union (downarrow A) by YELLOW_1:22;

then sup (waybelow A) c= sup (downarrow A) by YELLOW_1:22;

hence "\/" ((waybelow A),(InclPoset the topology of Y)) c= A by WAYBEL_0:34; :: thesis: verum