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 by WAYBEL_0:def 11;
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 q' = 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:24;
q' 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 q' <= y )
assume y in { (N . i) where i is Element of N : i >= j0 } ; :: thesis: q' <= y
then consider i1 being Element of N such that
A3: y = N . i1 and
A4: i1 >= j0 ;
reconsider i1' = i1 as Element of N ;
N . i1' in uparrow q by A1, A4;
hence q' <= y by A3, WAYBEL_0:18; :: thesis: verum

end;

then "/\" { (N . i) where i is Element of N : i >= j0 } ,R >= q' by YELLOW_0:33;
hence lim_inf N >= q by A2, YELLOW_0:def 2; :: thesis: verum