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: ( 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
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
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 A2, WAYBEL_0:25, YELLOW_9:47;
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 A8, SETFAM_1:3, TOPS_1:16;
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 (waybelow A) by TARSKI:def 4;
hence x in sup (waybelow A) by YELLOW_1:22; :: thesis: verum
end;
union (waybelow A) c= union (downarrow A) by WAYBEL_3:11, ZFMISC_1:77;
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