let T be complete Lawson TopLattice; :: thesis:
set S = the Scott TopAugmentation of T;
let N be eventually-filtered net of T; :: thesis:
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:

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

let u be Element of T; :: according to LATTICE3:def 8 :: thesis:
assume u in F ; :: thesis:
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

take ii ; :: according to WAYBEL_0:def 11 :: thesis:
let j be Element of N; :: thesis:
assume j >= ii ; :: thesis:
then N . j <= N . i by A8;
hence N . j in downarrow u by A7, WAYBEL_0:17; :: thesis:

end;

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

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:

end;

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

let A be Subset of T; :: thesis:
assume that
A13: inf F in A and
A14: A in K ; :: thesis:

per cases by A14, XBOOLE_0:def 3;

suppose A15: A in sigma T ; :: thesis:

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:

take the Element of N ; :: according to WAYBEL_0:def 11 :: thesis:
let j be Element of N; :: thesis:
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:

end;

end;

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

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:

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:
let j be Element of N; :: thesis:
assume j >= ii ; :: thesis:
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:

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: