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 by Th32;
A2: the carrier of (Net-Str D) = D by Th32;
set K = the prebasis of T;
now :: thesis: for A being Subset of T st sup D in A & A in the prebasis of T holds
Net-Str D is_eventually_in A
let A be Subset of T; :: thesis: ( sup D in A & A in the prebasis of T implies Net-Str D is_eventually_in A )
assume A3: sup D in A ; :: thesis: ( A in the prebasis of T implies Net-Str D is_eventually_in A )
A4: the prebasis of T c= the topology of T by TOPS_2:64;
assume A in the prebasis of T ; :: thesis: Net-Str D is_eventually_in A
then A is open by A4, PRE_TOPC:def 2;
then A is property(S) by WAYBEL19:36;
then consider y being Element of T such that
A5: y in D and
A6: for x being Element of T st x in D & x >= y holds
x in A by A3, WAYBEL11:def 3;
reconsider i = y as Element of (Net-Str D) by A5, Th32;
thus Net-Str D is_eventually_in A :: thesis: verum
proof
take i ; :: according to WAYBEL_0:def 11 :: thesis: for b1 being Element of the carrier of (Net-Str D) holds
( not i <= b1 or (Net-Str D) . b1 in A )
let j be Element of (Net-Str D); :: thesis: ( not i <= j or (Net-Str D) . j in A )
A7: j = (Net-Str D) . j by A1, A2;
A8: y = (Net-Str D) . i by A1, A2;
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 A2, A6, A7, A8; :: thesis: verum
end;
end;
hence sup D in Lim (Net-Str D) by WAYBEL19:25; :: thesis: verum