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
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;
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 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

deffunc H₁( Element of T) -> Element of bool the carrier of T = (uparrow c₁) ` ;
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 } c= the carrier of T

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { x where x is Element of T : (uparrow x) ` in F } or a in the carrier of T )
assume a in { x where x is Element of T : (uparrow x) ` in F } ; :: thesis: a in the carrier of T
then ex x being Element of T st
( a = x & (uparrow x) ` in F ) ;
hence a in the carrier of T ; :: thesis: verum

end;

reconsider z = "\/" { x where x is Element of T : (uparrow x) ` in F } ,T as Element of S by A2;
assume A4: X c= union F ; :: thesis: 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 S by A2;

now

assume not Y in sigma T ; :: thesis: contradiction
then Y in { ((uparrow x) ` ) where x is Element of T : verum } by A6, XBOOLE_0:def 3;
then consider y being Element of T such that
A7: Y = (uparrow y) ` ;
y in I2 by A6, A7;
then y <= "\/" { x where x is Element of T : (uparrow x) ` in F } ,T by YELLOW_2:24;
hence contradiction by A5, A7, YELLOW_9:1; :: thesis: verum

end;

then Z in the topology of S by YELLOW_9:51;
then A8: Z is open by PRE_TOPC:def 5;
then A9: Z is upper by WAYBEL11:15;
A10: z = sup J2 by YELLOW_0:17, A2, YELLOW_0:26
.= sup (finsups J2) by WAYBEL_0:55 ;
Z is property(S) by A8, WAYBEL11:15;
then consider y being Element of S such that
A11: y in finsups J2 and
A12: for x being Element of S st x in finsups J2 & x >= y holds
x in Z by A10, A5, WAYBEL11:def 3;
consider a being finite Subset of J2 such that
A13: y = "\/" a,S and
ex_sup_of a,S 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

proof

let i be set ; :: according to TARSKI:def 3 :: thesis: ( not i in {Y} \/ { ((uparrow c) ` ) where c is Element of T : c in a } or i in F )
assume that
A15: i in {Y} \/ { ((uparrow c) ` ) where c is Element of T : c in a } and
A16: not i in F ; :: thesis: contradiction
( i in {Y} or i in { ((uparrow c) ` ) where c is Element of T : c in a } ) by A15, XBOOLE_0:def 3;
then consider c being Element of T such that
A17: i = (uparrow c) ` and
A18: c in a by A6, A16, TARSKI:def 1;
c in J2 by A18;
then ex c9 being Element of T st
( c = c9 & (uparrow c9) ` in F ) ;
hence contradiction by A16, A17; :: thesis: verum

end;

A19: a is finite ;
{ H₁(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 ; :: 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 that
A20: u in X and
A21: not u in union G ; :: thesis: contradiction
reconsider u = u as Element of S by A20, A2;
A22: 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 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 )

proof

thus y <= y ; :: thesis: u is_>=_than a
let v be Element of S; :: according to LATTICE3:def 9 :: thesis: ( not v in a or v <= u )
assume A26: v in a ; :: thesis: v <= u
then v in J2 ;
then consider c being Element of T such that
A27: v = c and
(uparrow c) ` in F ;
(uparrow c) ` in { ((uparrow c) ` ) where c is Element of T : c in a } by A26, A27;
then A28: not u in (uparrow c) ` by A24, TARSKI:def 4;
(uparrow c) ` = (uparrow v) ` by A2, A27, WAYBEL_0:13;
hence v <= u by A28, YELLOW_9:1; :: thesis: verum

end;

then A29: u >= y by A13, YELLOW_0:32;
y in Z by A25, A11, A12;
hence contradiction by A29, A9, A23, 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