let L be complete Scott TopLattice; :: thesis: ( L is continuous implies ( L is compact & L is locally-compact & L is sober & L is Baire ) )
assume A1: L is continuous ; :: thesis: ( L is compact & L is locally-compact & L is sober & L is Baire )
A2: ( uparrow (Bottom L) = the carrier of L & [#] L = the carrier of L ) by Th10;
A3: for X being Subset of L st X is open holds
X is upper by WAYBEL11:def 4;
then uparrow (Bottom L) is compact by Th22;
hence L is compact by A2; :: thesis: ( L is locally-compact & L is sober & L is Baire )
thus A4: L is locally-compact :: thesis: ( L is sober & L is Baire )
proof
let x be Point of L; :: according to WAYBEL_3:def 9 :: thesis: for b1 being Element of bool the carrier of L holds
( not x in b1 or not b1 is open or ex b2 being Element of bool the carrier of L st
( x in Int b2 & b2 c= b1 & b2 is compact ) )
let X be Subset of L; :: thesis: ( not x in X or not X is open or ex b1 being Element of bool the carrier of L st
( x in Int b1 & b1 c= X & b1 is compact ) )
assume that
A5: x in X and
A6: X is open ; :: thesis: ex b1 being Element of bool the carrier of L st
( x in Int b1 & b1 c= X & b1 is compact )
reconsider x9 = x as Element of L ;
consider y being Element of L such that
A7: y << x9 and
A8: y in X by A1, A5, A6, WAYBEL11:43;
set Y = uparrow y;
set bas = { (wayabove q) where q is Element of L : q << x9 } ;
A9: { (wayabove q) where q is Element of L : q << x9 } is Basis of x by A1, WAYBEL11:44;
wayabove y in { (wayabove q) where q is Element of L : q << x9 } by A7;
then wayabove y is open by A9, YELLOW_8:12;
then A10: wayabove y c= Int (uparrow y) by TOPS_1:24, WAYBEL_3:11;
take uparrow y ; :: thesis: ( x in Int (uparrow y) & uparrow y c= X & uparrow y is compact )
x in wayabove y by A7;
hence x in Int (uparrow y) by A10; :: thesis: ( uparrow y c= X & uparrow y is compact )
X is upper by A6, WAYBEL11:def 4;
hence uparrow y c= X by A8, WAYBEL11:42; :: thesis: uparrow y is compact
thus uparrow y is compact by A3, Th22; :: thesis: verum
end;
sup_op L is jointly_Scott-continuous by A1, Th30;
hence L is sober by Th31; :: thesis: L is Baire
hence L is Baire by A4, WAYBEL12:44; :: thesis: verum