let R be complete LATTICE; :: thesis: for N being net of R
for p, q being Element of R st p is_S-limit_of N & N is_eventually_in downarrow q holds
p <= q
let N be net of R; :: thesis: for p, q being Element of R st p is_S-limit_of N & N is_eventually_in downarrow q holds
p <= q
let p, q be Element of R; :: thesis: ( p is_S-limit_of N & N is_eventually_in downarrow q implies p <= q )
assume that
A1: p <= lim_inf N and
A2: N is_eventually_in downarrow q ; :: according to WAYBEL11:def 7 :: thesis: p <= q
consider j0 being Element of N such that
A3: for i being Element of N st j0 <= i holds
N . i in downarrow q by A2, WAYBEL_0:def 11;
set X = { ("/\" { (N . i) where i is Element of N : i >= j } ,R) where j is Element of N : verum } ;
reconsider q' = q as Element of R ;
q' is_>=_than { ("/\" { (N . i) where i is Element of N : i >= j } ,R) where j is Element of N : verum }

proof

let x be Element of R; :: according to LATTICE3:def 9 :: thesis: ( not x in { ("/\" { (N . i) where i is Element of N : i >= j } ,R) where j is Element of N : verum } or x <= q' )
assume x in { ("/\" { (N . i) where i is Element of N : i >= j } ,R) where j is Element of N : verum } ; :: thesis: x <= q'
then consider j1 being Element of N such that
A4: x = "/\" { (N . i) where i is Element of N : i >= j1 } ,R ;
set Y = { (N . i) where i is Element of N : i >= j1 } ;
reconsider j1 = j1 as Element of N ;
consider j2 being Element of N such that
A5: ( j2 >= j0 & j2 >= j1 ) by YELLOW_6:def 5;
N . j2 in { (N . i) where i is Element of N : i >= j1 } by A5;
then A6: x <= N . j2 by A4, YELLOW_2:24;
N . j2 in downarrow q by A3, A5;
then N . j2 <= q' by WAYBEL_0:17;
hence x <= q' by A6, YELLOW_0:def 2; :: thesis: verum

end;

then lim_inf N <= q' by YELLOW_0:32;
hence p <= q by A1, YELLOW_0:def 2; :: thesis: verum