let Y be T_0-TopSpace; :: thesis: ( S6[Y] implies InclPoset the topology of Y is continuous )
assume A1: S6[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:
thus InclPoset the topology of Y is up-complete ; :: thesis:
let A be Element of (InclPoset the topology of Y); :: according to WAYBEL_3:def 5 :: thesis: 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 () :: according to XBOOLE_0:def 10 :: thesis: "\/" ((),(InclPoset the topology of Y)) c= A
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in sup () )
assume A3: x in A ; :: thesis: x in sup ()
then x in B ;
then reconsider x9 = x as Element of Y ;
reconsider B = B as open a_neighborhood of x9 by ;
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
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 b1 being Element of the carrier of (InclPoset the topology of Y) st
( b1 in D & ImH <= b1 ) )

A6: ( H1 is inaccessible & H1 is upper ) by ;
assume A <= sup D ; :: thesis: ex b1 being Element of the carrier of (InclPoset the topology of Y) st
( b1 in D & ImH <= b1 )

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 ;
then ImH c= d ;
hence ImH <= d by YELLOW_1:3; :: thesis: verum
end;
then ( x in Int mH & Int mH in waybelow A ) by CONNSP_2:def 1;
then x in union () by TARSKI:def 4;
hence x in sup () by YELLOW_1:22; :: thesis: verum
end;
union () c= union () by ;
then sup () c= union () by YELLOW_1:22;
then sup () c= sup () by YELLOW_1:22;
hence "\/" ((),(InclPoset the topology of Y)) c= A by WAYBEL_0:34; :: thesis: verum