let N be complete Lawson TopLattice; :: thesis: ( N is continuous iff ( N is meet-continuous & N is Hausdorff ) )
thus ( N is continuous implies ( N is meet-continuous & N is Hausdorff ) ) ; :: thesis: ( N is meet-continuous & N is Hausdorff implies N is continuous )
assume A1: ( N is meet-continuous & N is Hausdorff ) ; :: thesis: N is continuous
thus A2: for x being Element of N holds
( not waybelow x is empty & waybelow x is directed ) ; :: according to WAYBEL_3:def 6 :: thesis:
thus N is up-complete ; :: thesis:
for x, y being Element of N st not x <= y holds
ex u being Element of N st
( u << x & not u <= y )
proof
reconsider J = { (O \ ()) where O, F is Subset of N : ( O in sigma N & F is finite ) } as Basis of N by WAYBEL19:32;
set S = the Scott TopAugmentation of N;
A3: for N being Semilattice
for x, y being Element of N st ex u being Element of N st
( u << x & not u <= x "/\" y ) holds
ex u being Element of N st
( u << x & not u <= y )
proof
let N be Semilattice; :: thesis: for x, y being Element of N st ex u being Element of N st
( u << x & not u <= x "/\" y ) holds
ex u being Element of N st
( u << x & not u <= y )

let x, y be Element of N; :: thesis: ( ex u being Element of N st
( u << x & not u <= x "/\" y ) implies ex u being Element of N st
( u << x & not u <= y ) )

given u being Element of N such that A4: u << x and
A5: not u <= x "/\" y ; :: thesis: ex u being Element of N st
( u << x & not u <= y )

take u ; :: thesis: ( u << x & not u <= y )
thus u << x by A4; :: thesis: not u <= y
assume A6: u <= y ; :: thesis: contradiction
u <= x by ;
then u "/\" u <= x "/\" y by ;
hence contradiction by A5, YELLOW_0:25; :: thesis: verum
end;
let x, y be Element of N; :: thesis: ( not x <= y implies ex u being Element of N st
( u << x & not u <= y ) )

assume not x <= y ; :: thesis: ex u being Element of N st
( u << x & not u <= y )

then x "/\" y <> x by YELLOW_0:23;
then consider W, V being Subset of N such that
A7: W is open and
A8: V is open and
A9: x in W and
A10: x "/\" y in V and
A11: W misses V by A1;
V = union { G where G is Subset of N : ( G in J & G c= V ) } by ;
then consider K being set such that
A12: x "/\" y in K and
A13: K in { G where G is Subset of N : ( G in J & G c= V ) } by ;
consider V1 being Subset of N such that
A14: K = V1 and
A15: V1 in J and
A16: V1 c= V by A13;
consider U2, F being Subset of N such that
A17: V1 = U2 \ () and
A18: U2 in sigma N and
A19: F is finite by A15;
A20: RelStr(# the carrier of the Scott TopAugmentation of N, the InternalRel of the Scott TopAugmentation of N #) = RelStr(# the carrier of N, the InternalRel of N #) by YELLOW_9:def 4;
then reconsider x1 = x, y1 = y as Element of the Scott TopAugmentation of N ;
A21: ex_inf_of {x1,y1}, the Scott TopAugmentation of N by YELLOW_0:21;
reconsider U1 = U2 as Subset of the Scott TopAugmentation of N by A20;
reconsider WU1 = W /\ U2 as Subset of N ;
reconsider W1 = WU1 as Subset of the Scott TopAugmentation of N by A20;
A22: uparrow W1 = uparrow WU1 by ;
U2 in sigma the Scott TopAugmentation of N by ;
then A23: U1 is open by WAYBEL14:24;
then A24: U1 is upper by WAYBEL11:def 4;
WU1 c= uparrow F
proof
A25: W misses V1 by ;
A26: WU1 \ () c= U1 \ () by ;
let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in WU1 or w in uparrow F )
assume that
A27: w in WU1 and
A28: not w in uparrow F ; :: thesis: contradiction
A29: w in W by ;
w in WU1 \ () by ;
hence contradiction by A26, A17, A29, A25, XBOOLE_0:3; :: thesis: verum
end;
then WU1 is_coarser_than uparrow F by WAYBEL12:16;
then A30: uparrow WU1 c= uparrow F by YELLOW12:28;
A31: x1 "/\" y1 <= x1 by YELLOW_0:23;
x "/\" y = inf {x,y} by YELLOW_0:40
.= "/\" ({x1,y1}, the Scott TopAugmentation of N) by
.= x1 "/\" y1 by YELLOW_0:40 ;
then x1 "/\" y1 in U1 by ;
then x1 in U1 by ;
then A32: x in W1 by ;
W1 c= uparrow W1 by WAYBEL_0:16;
then A33: x in uparrow W1 by A32;
reconsider F1 = F as finite Subset of the Scott TopAugmentation of N by ;
A34: uparrow F1 = uparrow F by ;
N is correct Lawson TopAugmentation of the Scott TopAugmentation of N by ;
then U2 is open by ;
then uparrow W1 c= Int (uparrow F1) by ;
then A35: x in Int (uparrow F1) by A33;
the Scott TopAugmentation of N is meet-continuous by ;
then Int (uparrow F1) c= union { () where u is Element of the Scott TopAugmentation of N : u in F1 } by Th29;
then consider A being set such that
A36: x in A and
A37: A in { () where u is Element of the Scott TopAugmentation of N : u in F1 } by ;
consider u being Element of the Scott TopAugmentation of N such that
A38: A = wayabove u and
A39: u in F1 by A37;
reconsider u1 = u as Element of N by A20;
A40: wayabove u1 = wayabove u by ;
now :: thesis: ex u1 being Element of N st
( u1 << x & not u1 <= x "/\" y )
take u1 = u1; :: thesis: ( u1 << x & not u1 <= x "/\" y )
thus u1 << x by ; :: thesis: not u1 <= x "/\" y
uparrow u1 c= uparrow F by ;
then not x "/\" y in uparrow u1 by ;
hence not u1 <= x "/\" y by WAYBEL_0:18; :: thesis: verum
end;
then consider u2 being Element of N such that
A41: u2 << x and
A42: not u2 <= y by A3;
take u2 ; :: thesis: ( u2 << x & not u2 <= y )
thus ( u2 << x & not u2 <= y ) by ; :: thesis: verum
end;
hence N is satisfying_axiom_of_approximation by ; :: thesis: verum