let T be complete Lawson TopLattice; :: thesis:
consider S being 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 S = sigma T by YELLOW_9:51;
A2: RelStr(# the carrier of S,the InternalRel of S #) = 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 set ; :: 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 set such that
A6: ( i in dom the mapping of N & u = the mapping of N . i ) by FUNCT_1:def 5;
reconsider i = i as Element of N by A6;
consider ii being Element of N such that
A7: 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 A8: Cl (downarrow u) = downarrow u by PRE_TOPC:52;
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 A7;
hence N . j in downarrow u by A6, WAYBEL_0:17; :: thesis:

end;

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

end;

then A9: p <= inf N by A3, YELLOW_0:33;
inf N is_<=_than F by A3, YELLOW_0:33;
then A10: 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:52;
then A11: Cl F c= uparrow (inf N) by A10, PRE_TOPC:49;
p in Cl F by A5, WAYBEL_9:24;
then p >= inf N by A11, WAYBEL_0:18;
then p = inf N by A9, ORDERS_2:25;
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 A12: ( inf F in A & A in K ) ; :: thesis:

per cases by A12, XBOOLE_0:def 3;

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

then reconsider a = A as Subset of S by A1;
a is open by A1, A13, PRE_TOPC:def 5;
then a is upper by WAYBEL11:def 4;
then A14: A is upper by A2, WAYBEL_0:25;
consider i being Element of N;
thus N is_eventually_in A :: thesis:

take i ; :: according to WAYBEL_0:def 11 :: thesis:
let j be Element of N; :: thesis:
N . j in F by A4, FUNCT_1:def 5;
then N . j >= inf F by YELLOW_2:24;
hence ( not i <= j or N . j in A ) by A12, A14, WAYBEL_0:def 20; :: thesis:

end;

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

then consider x being Element of T such that
A15: A = (uparrow x) ` ;
not inf F >= x by A12, A15, YELLOW_9:1;
then not F is_>=_than x by YELLOW_0:33;
then consider y being Element of T such that
A16: ( y in F & not y >= x ) by LATTICE3:def 8;
consider i being set such that
A17: ( i in the carrier of N & y = the mapping of N . i ) by A4, A16, FUNCT_1:def 5;
thus N is_eventually_in A :: thesis:

reconsider i = i as Element of N by A17;
consider ii being Element of N such that
A18: 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 & N . i = y ) by A17, A18;
then not N . j >= x by A16, ORDERS_2:26;
hence N . j in A by A15, YELLOW_9:1; :: thesis:

end;

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