let T be complete TopLattice; ( T is Lawson implies ( T is T_1 & T is compact ) )
assume A1:
T is Lawson
; ( T is T_1 & T is compact )
for x being Point of T holds {x} is closed
by A1, Th38;
hence
T is T_1
by URYSOHN1:19; T is compact
set O1 = sigma T;
set O2 = { ((uparrow x) `) where x is Element of T : verum } ;
reconsider K = (sigma T) \/ { ((uparrow x) `) where x is Element of T : verum } as prebasis of T by A1, Th30;
set S = the Scott TopAugmentation of T;
the carrier of (InclPoset the topology of T) = the topology of T
by YELLOW_1:1;
then reconsider X = the carrier of T as Element of (InclPoset the topology of T) by PRE_TOPC:def 1;
A2:
RelStr(# the carrier of the Scott TopAugmentation of T, the InternalRel of the Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #)
by YELLOW_9:def 4;
for F being Subset of K st X c= union F holds
ex G being finite Subset of F st X c= union G
proof
deffunc H1(
Element of
T)
-> Element of
bool the
carrier of
T =
(uparrow c1) ` ;
let F be
Subset of
K;
( X c= union F implies ex G being finite Subset of F st X c= union G )
set I2 =
{ x where x is Element of T : (uparrow x) ` in F } ;
set x =
"\/" (
{ x where x is Element of T : (uparrow x) ` in F } ,
T);
A3:
{ x where x is Element of T : (uparrow x) ` in F } c= the
carrier of
T
reconsider z =
"\/" (
{ x where x is Element of T : (uparrow x) ` in F } ,
T) as
Element of the
Scott TopAugmentation of
T by A2;
assume A4:
X c= union F
;
ex G being finite Subset of F st X c= union G
"\/" (
{ x where x is Element of T : (uparrow x) ` in F } ,
T)
in X
;
then consider Y being
set such that A5:
"\/" (
{ x where x is Element of T : (uparrow x) ` in F } ,
T)
in Y
and A6:
Y in F
by A4, TARSKI:def 4;
Y in K
by A6;
then reconsider I2 =
{ x where x is Element of T : (uparrow x) ` in F } ,
Y =
Y as
Subset of
T by A3;
reconsider Z =
Y,
J2 =
I2 as
Subset of the
Scott TopAugmentation of
T by A2;
then
Z in the
topology of the
Scott TopAugmentation of
T
by YELLOW_9:51;
then A8:
Z is
open
;
then A9:
Z is
upper
by WAYBEL11:15;
A10:
z =
sup J2
by A2, YELLOW_0:17, YELLOW_0:26
.=
sup (finsups J2)
by WAYBEL_0:55
;
Z is
property(S)
by A8, WAYBEL11:15;
then consider y being
Element of the
Scott TopAugmentation of
T such that A11:
y in finsups J2
and A12:
for
x being
Element of the
Scott TopAugmentation of
T st
x in finsups J2 &
x >= y holds
x in Z
by A10, A5;
consider a being
finite Subset of
J2 such that A13:
y = "\/" (
a, the
Scott TopAugmentation of
T)
and
ex_sup_of a, the
Scott TopAugmentation of
T
by A11;
set AA =
{ ((uparrow c) `) where c is Element of T : c in a } ;
set G =
{Y} \/ { ((uparrow c) `) where c is Element of T : c in a } ;
A14:
{Y} \/ { ((uparrow c) `) where c is Element of T : c in a } c= F
A19:
a is
finite
;
{ H1(c) where c is Element of T : c in a } is
finite
from FRAENKEL:sch 21(A19);
then reconsider G =
{Y} \/ { ((uparrow c) `) where c is Element of T : c in a } as
finite Subset of
F by A14;
take
G
;
X c= union G
let u be
object ;
TARSKI:def 3 ( not u in X or u in union G )
assume that A20:
u in X
and A21:
not
u in union G
;
contradiction
reconsider u =
u as
Element of the
Scott TopAugmentation of
T by A20, A2;
A22:
union G =
(union {Y}) \/ (union { ((uparrow c) `) where c is Element of T : c in a } )
by ZFMISC_1:78
.=
Y \/ (union { ((uparrow c) `) where c is Element of T : c in a } )
by ZFMISC_1:25
;
then A23:
not
u in Y
by A21, XBOOLE_0:def 3;
A24:
not
u in union { ((uparrow c) `) where c is Element of T : c in a }
by A22, A21, XBOOLE_0:def 3;
A25:
(
y <= y &
u is_>=_than a )
then A29:
u >= y
by A13, YELLOW_0:32;
y in Z
by A25, A11, A12;
hence
contradiction
by A29, A9, A23;
verum
end;
then
X << X
by WAYBEL_7:31;
then
X is compact
;
hence
T is compact
by WAYBEL_3:37; verum