let T be complete Lawson TopLattice; :: thesis: for N being eventually-filtered net of T holds Lim N = {(inf N)}
set S = the Scott TopAugmentation of T;
let N be eventually-filtered net of T; :: thesis: Lim N = {(inf N)}
reconsider F = rng the mapping of N as non empty filtered Subset of T by Th43;
A1: the topology of the Scott TopAugmentation of T = sigma T by YELLOW_9:51;
A2: RelStr(# the carrier of the Scott TopAugmentation of T, the InternalRel of the Scott TopAugmentation of T #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def 4;
A3: inf N = Inf by WAYBEL_9:def 2
.= "/\" (F,T) by YELLOW_2:def 6 ;
A4: dom the mapping of N = the carrier of N by FUNCT_2:def 1;
thus Lim N c= {(inf N)} :: according to XBOOLE_0:def 10 :: thesis: {(inf N)} c= Lim N

proof

let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in Lim N or p in {(inf N)} )
assume A5: p in Lim N ; :: thesis: p in {(inf N)}
then reconsider p = p as Element of T ;
p is_<=_than F

proof

let u be Element of T; :: according to LATTICE3:def 8 :: thesis: ( not u in F or p <= u )
assume u in F ; :: thesis: p <= u
then consider i being object such that
A6: i in dom the mapping of N and
A7: u = the mapping of N . i by FUNCT_1:def 3;
reconsider i = i as Element of N by A6;
consider ii being Element of N such that
A8: for k being Element of N st ii <= k holds
N . i >= N . k by WAYBEL_0:12;
downarrow u is closed by WAYBEL19:38;
then A9: Cl (downarrow u) = downarrow u by PRE_TOPC:22;
N is_eventually_in downarrow u

proof

take ii ; :: according to WAYBEL_0:def 11 :: thesis: for b₁ being Element of the carrier of N holds
( not ii <= b₁ or N . b₁ in downarrow u )
let j be Element of N; :: thesis: ( not ii <= j or N . j in downarrow u )
assume j >= ii ; :: thesis: N . j in downarrow u
then N . j <= N . i by A8;
hence N . j in downarrow u by A7, WAYBEL_0:17; :: thesis: verum

end;

then Lim N c= downarrow u by A9, WAYBEL19:26;
hence p <= u by A5, WAYBEL_0:17; :: thesis: verum

end;

then A10: p <= inf N by A3, YELLOW_0:33;
inf N is_<=_than F by A3, YELLOW_0:33;
then A11: F c= uparrow (inf N) by YELLOW_2:2;
uparrow (inf N) is closed by WAYBEL19:38;
then Cl (uparrow (inf N)) = uparrow (inf N) by PRE_TOPC:22;
then A12: Cl F c= uparrow (inf N) by A11, PRE_TOPC:19;
p in Cl F by A5, WAYBEL_9:24;
then p >= inf N by A12, WAYBEL_0:18;
then p = inf N by A10, ORDERS_2:2;
hence p in {(inf N)} by TARSKI:def 1; :: thesis: verum

end;

reconsider K = (sigma T) \/ { ((uparrow x) `) where x is Element of T : verum } as prebasis of T by WAYBEL19:30;

now :: thesis: for A being Subset of T st inf F in A & A in K holds
N is_eventually_in A

let A be Subset of T; :: thesis: ( inf F in A & A in K implies N is_eventually_in b₁ )
assume that
A13: inf F in A and
A14: A in K ; :: thesis: N is_eventually_in b₁

per cases ( A in sigma T or A in { ((uparrow x) `) where x is Element of T : verum } ) by A14, XBOOLE_0:def 3;

suppose A15: A in sigma T ; :: thesis: N is_eventually_in b₁

then reconsider a = A as Subset of the Scott TopAugmentation of T by A1;
a is open by A1, A15, PRE_TOPC:def 2;
then a is upper by WAYBEL11:def 4;
then A16: A is upper by A2, WAYBEL_0:25;
set i = the Element of N;
thus N is_eventually_in A :: thesis: verum

proof

take the Element of N ; :: according to WAYBEL_0:def 11 :: thesis: for b₁ being Element of the carrier of N holds
( not the Element of N <= b₁ or N . b₁ in A )
let j be Element of N; :: thesis: ( not the Element of N <= j or N . j in A )
N . j in F by A4, FUNCT_1:def 3;
then N . j >= inf F by YELLOW_2:22;
hence ( not the Element of N <= j or N . j in A ) by A13, A16; :: thesis: verum

end;

end;

suppose A in { ((uparrow x) `) where x is Element of T : verum } ; :: thesis: N is_eventually_in b₁

then consider x being Element of T such that
A17: A = (uparrow x) ` ;
not inf F >= x by A13, A17, YELLOW_9:1;
then not F is_>=_than x by YELLOW_0:33;
then consider y being Element of T such that
A18: y in F and
A19: not y >= x ;
consider i being object such that
A20: i in the carrier of N and
A21: y = the mapping of N . i by A4, A18, FUNCT_1:def 3;
thus N is_eventually_in A :: thesis: verum

proof

reconsider i = i as Element of N by A20;
consider ii being Element of N such that
A22: for k being Element of N st ii <= k holds
N . i >= N . k by WAYBEL_0:12;
take ii ; :: according to WAYBEL_0:def 11 :: thesis: for b₁ being Element of the carrier of N holds
( not ii <= b₁ or N . b₁ in A )
let j be Element of N; :: thesis: ( not ii <= j or N . j in A )
assume j >= ii ; :: thesis: N . j in A
then N . j <= N . i by A22;
then not N . j >= x by A19, A21, ORDERS_2:3;
hence N . j in A by A17, YELLOW_9:1; :: thesis: verum

end;

end;

end;

end;

then inf F in Lim N by WAYBEL19:25;
hence {(inf N)} c= Lim N by A3, ZFMISC_1:31; :: thesis: verum