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: sup (waybelow x) <= x by Th9;
A3: { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } c= waybelow x

proof

let d be object ; :: 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
A4: inf V = d and
A5: x in V and
A6: V in sigma L ;
V is open by A6, Th24;
then inf V << x by A5, Th26;
hence d in waybelow x by A4; :: 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 A7: "\/" ( { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L) <= sup (waybelow x) by A3, YELLOW_0:34;
x = "\/" ( { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L) by A1;
hence x = "\/" ((waybelow x),L) by A7, A2, ORDERS_2:2; :: thesis: verum