let T be complete TopLattice; :: thesis: ( T is Lawson implies ( T is T_1 & T is compact ) )
assume A1:
T is Lawson
; :: thesis: ( 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:27; :: thesis: T is compact
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;
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;
consider S being Scott TopAugmentation of T;
A2:
RelStr(# the carrier of S,the InternalRel of S #) = 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
let F be
Subset of
K;
:: thesis: ( 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 } ,
T in X
;
assume
X c= union F
;
:: thesis: ex G being finite Subset of F st X c= union G
then consider Y being
set such that A4:
(
"\/" { x where x is Element of T : (uparrow x) ` in F } ,
T in Y &
Y in F )
by A3, TARSKI:def 4;
A5:
Y in K
by A4;
{ x where x is Element of T : (uparrow x) ` in F } c= the
carrier of
T
then reconsider I2 =
{ x where x is Element of T : (uparrow x) ` in F } ,
Y =
Y as
Subset of
T by A5;
reconsider Z =
Y,
J2 =
I2 as
Subset of
S by A2;
reconsider z =
"\/" { x where x is Element of T : (uparrow x) ` in F } ,
T as
Element of
S by A2;
then
Z in the
topology of
S
by YELLOW_9:51;
then
Z is
open
by PRE_TOPC:def 5;
then A7:
(
Z is
property(S) &
Z is
upper )
by WAYBEL11:15;
ex_sup_of I2,
T
by YELLOW_0:17;
then z =
sup J2
by A2, YELLOW_0:26
.=
sup (finsups J2)
by WAYBEL_0:55
;
then consider y being
Element of
S such that A8:
y in finsups J2
and A9:
for
x being
Element of
S st
x in finsups J2 &
x >= y holds
x in Z
by A4, A7, WAYBEL11:def 3;
consider a being
finite Subset of
J2 such that A10:
(
y = "\/" a,
S &
ex_sup_of a,
S )
by A8;
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 } ;
A11:
{Y} \/ { ((uparrow c) ` ) where c is Element of T : c in a } c= F
A14:
a is
finite
;
deffunc H1(
Element of
T)
-> Element of
bool the
carrier of
T =
(uparrow c1) ` ;
{ H1(c) where c is Element of T : c in a } is
finite
from FRAENKEL:sch 21(A14);
then reconsider G =
{Y} \/ { ((uparrow c) ` ) where c is Element of T : c in a } as
finite Subset of
F by A11;
take
G
;
:: thesis: X c= union G
let u be
set ;
:: according to TARSKI:def 3 :: thesis: ( not u in X or u in union G )
assume A15:
(
u in X & not
u in union G )
;
:: thesis: contradiction
then reconsider u =
u as
Element of
S by A2;
union G =
(union {Y}) \/ (union { ((uparrow c) ` ) where c is Element of T : c in a } )
by ZFMISC_1:96
.=
Y \/ (union { ((uparrow c) ` ) where c is Element of T : c in a } )
by ZFMISC_1:31
;
then A16:
( not
u in Y & not
u in union { ((uparrow c) ` ) where c is Element of T : c in a } )
by A15, XBOOLE_0:def 3;
(
y <= y &
u is_>=_than a )
then
(
u >= y &
y in Z )
by A8, A9, A10, YELLOW_0:32;
hence
contradiction
by A7, A16, WAYBEL_0:def 20;
:: thesis: verum
end;
then
X << X
by WAYBEL_7:35;
then
X is compact
by WAYBEL_3:def 2;
hence
T is compact
by WAYBEL_3:37; :: thesis: verum