let T be complete Lawson TopLattice; :: thesis: for D being non empty directed Subset of T holds sup D in Lim (Net-Str D)
let D be non empty directed Subset of T; :: thesis: sup D in Lim (Net-Str D)
set N = Net-Str D;
A1: ( the mapping of (Net-Str D) = id D & the carrier of (Net-Str D) = D ) by Th32;
consider K being prebasis of T;

now

let A be Subset of T; :: thesis: ( sup D in A & A in K implies Net-Str D is_eventually_in A )
assume A2: sup D in A ; :: thesis: ( A in K implies Net-Str D is_eventually_in A )
A3: K c= the topology of T by CANTOR_1:def 5;
assume A in K ; :: thesis: Net-Str D is_eventually_in A
then A is open by A3, PRE_TOPC:def 5;
then A is property(S) by WAYBEL19:36;
then consider y being Element of T such that
A4: y in D and
A5: for x being Element of T st x in D & x >= y holds
x in A by A2, WAYBEL11:def 3;
reconsider i = y as Element of (Net-Str D) by A4, Th32;
thus Net-Str D is_eventually_in A :: thesis: verum

proof

take i ; :: according to WAYBEL_0:def 11 :: thesis: for b₁ being Element of the carrier of (Net-Str D) holds
( not i <= b₁ or (Net-Str D) . b₁ in A )
let j be Element of (Net-Str D); :: thesis: ( not i <= j or (Net-Str D) . j in A )
A6: ( j = (Net-Str D) . j & y = (Net-Str D) . i ) by A1, FUNCT_1:34;
assume j >= i ; :: thesis: (Net-Str D) . j in A
then (Net-Str D) . j >= (Net-Str D) . i by Th34;
hence (Net-Str D) . j in A by A1, A5, A6; :: thesis: verum

end;

end;

hence sup D in Lim (Net-Str D) by WAYBEL19:25; :: thesis: verum