let Y be T_0-TopSpace; :: thesis: ( S₆[Y] implies InclPoset the topology of Y is continuous )
assume A1: S₆[Y] ; :: thesis: InclPoset the topology of Y is continuous
set L = InclPoset the topology of Y;
consider S being Scott TopAugmentation of InclPoset the topology of Y;
A2: RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of (InclPoset the topology of Y),the InternalRel of (InclPoset the topology of Y) #) by YELLOW_9:def 4;
A3: the carrier of (InclPoset the topology of Y) = the topology of Y by YELLOW_1:1;
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)
A in the topology of Y by A3;
then reconsider B = A as open Subset of Y by PRE_TOPC:def 5;
thus A c= sup (waybelow A) :: according to XBOOLE_0:def 10 :: thesis: "\/" (waybelow A),(InclPoset the topology of Y) c= A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in sup (waybelow A) )
assume A4: x in A ; :: thesis: x in sup (waybelow A)
then x in B ;
then reconsider x' = x as Element of Y ;
reconsider B = B as open a_neighborhood of x' by A4, CONNSP_2:5;
consider H being open Subset of S such that
A5: ( B in H & meet H is a_neighborhood of x' ) by A1;
reconsider H1 = H as Subset of (InclPoset the topology of Y) by A2;
reconsider mH = meet H as a_neighborhood of x' by A5;
A6: x in Int mH by CONNSP_2:def 1;
Int mH in the topology of Y by PRE_TOPC:def 5;
then reconsider ImH = Int mH as Element of (InclPoset the topology of Y) by YELLOW_1:1;
ImH << A

proof

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₁ being Element of the carrier of (InclPoset the topology of Y) st
( b₁ in D & ImH <= b₁ ) )
assume A7: A <= sup D ; :: thesis: ex b₁ being Element of the carrier of (InclPoset the topology of Y) st
( b₁ in D & ImH <= b₁ )
A8: ( H1 is inaccessible_by_directed_joins & H1 is upper ) by A2, WAYBEL_0:25, YELLOW_9:47;
then sup D in H1 by A5, A7, WAYBEL_0:def 20;
then D meets H1 by A8, WAYBEL11:def 1;
then consider d being set such that
A9: ( d in D & d in H1 ) by XBOOLE_0:3;
reconsider d = d as Element of (InclPoset the topology of Y) by A9;
take d ; :: thesis: ( d in D & ImH <= d )
thus d in D by A9; :: thesis: ImH <= d
A10: Int mH c= mH by TOPS_1:44;
mH c= d by A9, SETFAM_1:4;
then ImH c= d by A10, XBOOLE_1:1;
hence ImH <= d by YELLOW_1:3; :: thesis: verum

end;

then Int mH in waybelow A ;
then x in union (waybelow A) by A6, TARSKI:def 4;
hence x in sup (waybelow A) by YELLOW_1:22; :: thesis: verum

end;

waybelow A c= downarrow A by WAYBEL_3:11;
then union (waybelow A) c= union (downarrow A) by ZFMISC_1:95;
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