let L be complete Scott TopLattice; :: thesis: for X being Subset of L st L is continuous & X in sigma L holds
X = union { (wayabove x) where x is Element of L : x in X }
let X be Subset of L; :: thesis: ( L is continuous & X in sigma L implies X = union { (wayabove x) where x is Element of L : x in X } )
assume that
A1: L is continuous and
A2: X in sigma L ; :: thesis: X = union { (wayabove x) where x is Element of L : x in X }
A3: X is open by A2, Th24;
set WAV = { (wayabove x) where x is Element of L : x in X } ;

now

let x be set ; :: thesis: ( ( x in X implies x in union { (wayabove x) where x is Element of L : x in X } ) & ( x in union { (wayabove x) where x is Element of L : x in X } implies x in X ) )

hereby :: thesis: ( x in union { (wayabove x) where x is Element of L : x in X } implies x in X )

assume A4: x in X ; :: thesis: x in union { (wayabove x) where x is Element of L : x in X }
then reconsider x' = x as Element of L ;
consider q being Element of L such that
A5: ( q << x' & q in X ) by A1, A3, A4, WAYBEL11:43;
A6: x' in wayabove q by A5;
wayabove q in { (wayabove x) where x is Element of L : x in X } by A5;
hence x in union { (wayabove x) where x is Element of L : x in X } by A6, TARSKI:def 4; :: thesis: verum

end;

assume x in union { (wayabove x) where x is Element of L : x in X } ; :: thesis: x in X
then consider Y being set such that
A7: ( x in Y & Y in { (wayabove x) where x is Element of L : x in X } ) by TARSKI:def 4;
consider q being Element of L such that
A8: ( Y = wayabove q & q in X ) by A7;
X is upper by A3, WAYBEL11:def 4;
then A9: uparrow q c= X by A8, WAYBEL11:42;
wayabove q c= uparrow q by WAYBEL_3:11;
then Y c= X by A8, A9, XBOOLE_1:1;
hence x in X by A7; :: thesis: verum

end;

hence X = union { (wayabove x) where x is Element of L : x in X } by TARSKI:2; :: thesis: verum