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;
set X = { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } ;
reconsider q9 = q as Element of R ;
q9 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 <= q9 )
assume x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } ; :: thesis: x <= q9
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 and
A6: j2 >= j1 by YELLOW_6:def 3;
N . j2 in { (N . i) where i is Element of N : i >= j1 } by A6;
then A7: x <= N . j2 by A4, YELLOW_2:22;
N . j2 in downarrow q by A3, A5;
then N . j2 <= q9 by WAYBEL_0:17;
hence x <= q9 by A7, YELLOW_0:def 2; :: thesis: verum

end;

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