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 }
set WAV = { (wayabove x) where x is Element of L : x in X } ;
A3: X is open by A2, Th24;
now :: thesis: for x being object holds
( ( 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 ) )
let x be object ; :: 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 x9 = x as Element of L ;
consider q being Element of L such that
A5: ( q << x9 & q in X ) by A1, A3, A4, WAYBEL11:43;
( x9 in wayabove q & 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 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
A6: x in Y and
A7: 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 and
A9: q in X by A7;
A10: wayabove q c= uparrow q by WAYBEL_3:11;
X is upper by A3, WAYBEL11:def 4;
then uparrow q c= X by A9, WAYBEL11:42;
then Y c= X by A8, A10;
hence x in X by A6; :: thesis: verum
end;
hence X = union { (wayabove x) where x is Element of L : x in X } by TARSKI:2; :: thesis: verum