let N be complete Lawson TopLattice; ( N is continuous iff ( N is meet-continuous & N is Hausdorff ) )
thus
( N is continuous implies ( N is meet-continuous & N is Hausdorff ) )
; ( N is meet-continuous & N is Hausdorff implies N is continuous )
assume A1:
( N is meet-continuous & N is Hausdorff )
; N is continuous
thus A2:
for x being Element of N holds
( not waybelow x is empty & waybelow x is directed )
; WAYBEL_3:def 6 ( N is up-complete & N is satisfying_axiom_of_approximation )
thus
N is up-complete
; N is satisfying_axiom_of_approximation
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 \ (uparrow F)) 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 )
let x,
y be
Element of
N;
( not x <= y implies ex u being Element of N st
( u << x & not u <= y ) )
assume
not
x <= y
;
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 A8, YELLOW_8:9;
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 A10, TARSKI:def 4;
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 \ (uparrow F)
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 A20, WAYBEL_0:13;
U2 in sigma the
Scott TopAugmentation of
N
by A20, A18, YELLOW_9:52;
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 A11, A16, XBOOLE_1:63;
A26:
WU1 \ (uparrow F) c= U1 \ (uparrow F)
by XBOOLE_1:17, XBOOLE_1:33;
let w be
object ;
TARSKI:def 3 ( not w in WU1 or w in uparrow F )
assume that A27:
w in WU1
and A28:
not
w in uparrow F
;
contradiction
A29:
w in W
by A27, XBOOLE_0:def 4;
w in WU1 \ (uparrow F)
by A27, A28, XBOOLE_0:def 5;
hence
contradiction
by A26, A17, A29, A25, XBOOLE_0:3;
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 A20, A21, YELLOW_0:27
.=
x1 "/\" y1
by YELLOW_0:40
;
then
x1 "/\" y1 in U1
by A12, A14, A17, XBOOLE_0:def 5;
then
x1 in U1
by A24, A31;
then A32:
x in W1
by A9, XBOOLE_0:def 4;
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 A20, A19;
A34:
uparrow F1 = uparrow F
by A20, WAYBEL_0:13;
N is
correct Lawson TopAugmentation of the
Scott TopAugmentation of
N
by A20, YELLOW_9:def 4;
then
U2 is
open
by A23, WAYBEL19:37;
then
uparrow W1 c= Int (uparrow F1)
by A7, A1, A30, A22, A34, Th15, TOPS_1:24;
then A35:
x in Int (uparrow F1)
by A33;
the
Scott TopAugmentation of
N is
meet-continuous
by A1, A20, YELLOW12:14;
then
Int (uparrow F1) c= union { (wayabove u) 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 { (wayabove u) where u is Element of the Scott TopAugmentation of N : u in F1 }
by A35, TARSKI:def 4;
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 A20, YELLOW12:13;
then consider u2 being
Element of
N such that A41:
u2 << x
and A42:
not
u2 <= y
by A3;
take
u2
;
( u2 << x & not u2 <= y )
thus
(
u2 << x & not
u2 <= y )
by A41, A42;
verum
end;
hence
N is satisfying_axiom_of_approximation
by A2, WAYBEL_3:24; verum