let L be complete Scott TopLattice; :: thesis: ( ( for x being Element of L holds x = "\/" { (inf X) where X is Subset of L : ( x in X & X in sigma L ) } ,L ) implies L is continuous )
assume A1: for x being Element of L holds x = "\/" { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L ; :: thesis: L is continuous
thus for x being Element of L holds
( not waybelow x is empty & waybelow x is directed ) ; :: according to WAYBEL_3:def 6 :: thesis: ( L is up-complete & L is satisfying_axiom_of_approximation )
thus L is up-complete ; :: thesis: L is satisfying_axiom_of_approximation
let x be Element of L; :: according to WAYBEL_3:def 5 :: thesis: x = "\/" (waybelow x),L
set VV = { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ;
A2: { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } c= waybelow x

proof

let d be set ; :: according to TARSKI:def 3 :: thesis: ( not d in { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } or d in waybelow x )
assume d in { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ; :: thesis: d in waybelow x
then consider V being Subset of L such that
A3: ( inf V = d & x in V & V in sigma L ) ;
V is open by A3, Th24;
then inf V << x by A3, Th26;
hence d in waybelow x by A3; :: thesis: verum

end;

( ex_sup_of { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L & ex_sup_of waybelow x,L ) by YELLOW_0:17;
then A4: "\/" { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L <= sup (waybelow x) by A2, YELLOW_0:34;
( x = "\/" { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L & sup (waybelow x) <= x ) by A1, Th9;
hence x = "\/" (waybelow x),L by A4, ORDERS_2:25; :: thesis: verum