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: ( N is up-complete & N is satisfying_axiom_of_approximation )

thus N is up-complete ; :: thesis: 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 )

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: ( N is up-complete & N is satisfying_axiom_of_approximation )

thus N is up-complete ; :: thesis: 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

hence
N is satisfying_axiom_of_approximation
by A2, WAYBEL_3:24; :: thesis: verum
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 )

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

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;

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 A41, A42; :: thesis: verum

end;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 x, y be Element of N; :: thesis: ( not x <= y implies ex u being Element of N st
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 A4, WAYBEL_3:1;

then u "/\" u <= x "/\" y by A6, YELLOW_3:2;

hence contradiction by A5, YELLOW_0:25; :: thesis: verum

end;( 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 A4, WAYBEL_3:1;

then u "/\" u <= x "/\" y by A6, YELLOW_3:2;

hence contradiction by A5, YELLOW_0:25; :: thesis: verum

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

then
WU1 is_coarser_than uparrow F
by WAYBEL12:16;
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 ; :: 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 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; :: thesis: verum

end;A26: WU1 \ (uparrow F) c= U1 \ (uparrow F) by XBOOLE_1:17, XBOOLE_1:33;

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 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; :: thesis: verum

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;

now :: thesis: ex u1 being Element of N st

( u1 << x & not u1 <= x "/\" y )

then consider u2 being Element of N such that ( u1 << x & not u1 <= x "/\" y )

take u1 = u1; :: thesis: ( u1 << x & not u1 <= x "/\" y )

thus u1 << x by A36, A38, A40, WAYBEL_3:8; :: thesis: not u1 <= x "/\" y

uparrow u1 c= uparrow F by A39, YELLOW12:30;

then not x "/\" y in uparrow u1 by A12, A14, A17, XBOOLE_0:def 5;

hence not u1 <= x "/\" y by WAYBEL_0:18; :: thesis: verum

end;thus u1 << x by A36, A38, A40, WAYBEL_3:8; :: thesis: not u1 <= x "/\" y

uparrow u1 c= uparrow F by A39, YELLOW12:30;

then not x "/\" y in uparrow u1 by A12, A14, A17, XBOOLE_0:def 5;

hence not u1 <= x "/\" y by WAYBEL_0:18; :: thesis: verum

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 A41, A42; :: thesis: verum