let R be complete LATTICE; :: thesis: for N being net of R
for p, q being Element of R st N is_eventually_in uparrow q holds
lim_inf N >= q
let N be net of R; :: thesis: for p, q being Element of R st N is_eventually_in uparrow q holds
lim_inf N >= q
let p, q be Element of R; :: thesis: ( N is_eventually_in uparrow q implies lim_inf N >= q )
assume N is_eventually_in uparrow q ; :: thesis: lim_inf N >= q
then consider j0 being Element of N such that
A1: for i being Element of N st j0 <= i holds
N . i in uparrow q ;
set X = { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } ;
set Y = { (N . i) where i is Element of N : i >= j0 } ;
reconsider q9 = q as Element of R ;
"/\" ( { (N . i) where i is Element of N : i >= j0 } ,R) in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } ;
then A2: lim_inf N >= "/\" ( { (N . i) where i is Element of N : i >= j0 } ,R) by YELLOW_2:22;
q9 is_<=_than { (N . i) where i is Element of N : i >= j0 }
proof
let y be Element of R; :: according to LATTICE3:def 8 :: thesis: ( not y in { (N . i) where i is Element of N : i >= j0 } or q9 <= y )
assume y in { (N . i) where i is Element of N : i >= j0 } ; :: thesis: q9 <= y
then consider i1 being Element of N such that
A3: y = N . i1 and
A4: i1 >= j0 ;
reconsider i19 = i1 as Element of N ;
N . i19 in uparrow q by A1, A4;
hence q9 <= y by A3, WAYBEL_0:18; :: thesis: verum
end;
then "/\" ( { (N . i) where i is Element of N : i >= j0 } ,R) >= q9 by YELLOW_0:33;
hence lim_inf N >= q by A2, YELLOW_0:def 2; :: thesis: verum