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))) ` ;
assume A2: x <> sup (waybelow x) ; :: thesis: contradiction
A3: sup (waybelow x) <= x by Th9;
then A4: x in (downarrow (sup (waybelow x))) ` by XBOOLE_0:def 5;
set Z = { (wayabove z) where z is Element of L : z in (downarrow (sup (waybelow x))) ` } ;
A5: sup (waybelow x) is_>=_than waybelow x by YELLOW_0:32;
(downarrow (sup (waybelow x))) ` is open by WAYBEL11:12;
then (downarrow (sup (waybelow x))) ` in sigma L by 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 and
A7: 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
A8: Y = wayabove z and
A9: z in (downarrow (sup (waybelow x))) ` by A7;
z << x by A6, A8, WAYBEL_3:8;
then z in waybelow x ;
then z <= sup (waybelow x) by A5, LATTICE3:def 9;
then z in downarrow (sup (waybelow x)) by WAYBEL_0:17;
hence contradiction by A9, XBOOLE_0:def 5; :: thesis: verum