let L be complete Scott TopLattice; :: thesis: ( ( for X being Subset of L st X in sigma L holds
X = union { (wayabove x) where x is Element of L : x in X } ) implies L is continuous )
assume A1: for X being Subset of L st X in sigma L holds
X = union { (wayabove x) where x is Element of L : x in X } ; :: 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 y = sup (waybelow x);
set X = (downarrow (sup (waybelow x))) ` ;
A2: sup (waybelow x) <= x by Th9;
assume A3: x <> sup (waybelow x) ; :: thesis: contradiction

now

assume x in downarrow (sup (waybelow x)) ; :: thesis: contradiction
then x <= sup (waybelow x) by WAYBEL_0:17;
hence contradiction by A2, A3, ORDERS_2:25; :: thesis: verum

end;

then A4: x in (downarrow (sup (waybelow x))) ` by XBOOLE_0:def 5;
A5: (downarrow (sup (waybelow x))) ` is open by WAYBEL11:12;
set Z = { (wayabove z) where z is Element of L : z in (downarrow (sup (waybelow x))) ` } ;
(downarrow (sup (waybelow x))) ` in sigma L by A5, Th24;
then (downarrow (sup (waybelow x))) ` = union { (wayabove z) where z is Element of L : z in (downarrow (sup (waybelow x))) ` } by A1;
then consider Y being set such that
A6: ( x in Y & Y in { (wayabove z) where z is Element of L : z in (downarrow (sup (waybelow x))) ` } ) by A4, TARSKI:def 4;
consider z being Element of L such that
A7: ( Y = wayabove z & z in (downarrow (sup (waybelow x))) ` ) by A6;
z << x by A6, A7, WAYBEL_3:8;
then A8: z in waybelow x ;
sup (waybelow x) is_>=_than waybelow x by YELLOW_0:32;
then z <= sup (waybelow x) by A8, LATTICE3:def 9;
then z in downarrow (sup (waybelow x)) by WAYBEL_0:17;
hence contradiction by A7, XBOOLE_0:def 5; :: thesis: verum