let L be complete Scott TopLattice; ( ( 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)
; L is continuous
thus
for x being Element of L holds
( not waybelow x is empty & waybelow x is directed )
; WAYBEL_3:def 6 ( L is up-complete & L is satisfying_axiom_of_approximation )
thus
L is up-complete
; L is satisfying_axiom_of_approximation
let x be Element of L; WAYBEL_3:def 5 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
( 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; verum