let R be complete LATTICE; :: thesis: for N being constant net of R holds the_value_of N = lim_inf N
let N be constant net of R; :: thesis: the_value_of N = lim_inf N
set X = { ("/\" { (N . i) where i is Element of N : i >= j } ,R) where j is Element of N : verum } ;
consider j being Element of N;
A1: N . j is_>=_than { ("/\" { (N . i) where i is Element of N : i >= j } ,R) where j is Element of N : verum }

proof

let b be Element of R; :: according to LATTICE3:def 9 :: thesis: ( not b in { ("/\" { (N . i) where i is Element of N : i >= j } ,R) where j is Element of N : verum } or b <= N . j )
assume b in { ("/\" { (N . i) where i is Element of N : i >= j } ,R) where j is Element of N : verum } ; :: thesis: b <= N . j
then consider j0 being Element of N such that
A2: b = "/\" { (N . i) where i is Element of N : i >= j0 } ,R ;
reconsider j0 = j0 as Element of N ;
consider i0 being Element of N such that
A3: i0 >= j0 and
i0 >= j0 by YELLOW_6:def 5;
A4: N . i0 in { (N . i) where i is Element of N : i >= j0 } by A3;
N . i0 = the_value_of N by YELLOW_6:25
.= N . j by YELLOW_6:25 ;
hence b <= N . j by A2, A4, YELLOW_2:24; :: thesis: verum

end;

A5: for b being Element of R st b is_>=_than { ("/\" { (N . i) where i is Element of N : i >= j } ,R) where j is Element of N : verum } holds
N . j <= b

proof

let b be Element of R; :: thesis: ( b is_>=_than { ("/\" { (N . i) where i is Element of N : i >= j } ,R) where j is Element of N : verum } implies N . j <= b )
set Y = { (N . i) where i is Element of N : i >= j } ;
A6: "/\" { (N . i) where i is Element of N : i >= j } ,R in { ("/\" { (N . i) where i is Element of N : i >= j } ,R) where j is Element of N : verum } ;
assume b is_>=_than { ("/\" { (N . i) where i is Element of N : i >= j } ,R) where j is Element of N : verum } ; :: thesis: N . j <= b
then A7: b >= "/\" { (N . i) where i is Element of N : i >= j } ,R by A6, LATTICE3:def 9;
A8: N . j is_<=_than { (N . i) where i is Element of N : i >= j }

proof

let c be Element of R; :: according to LATTICE3:def 8 :: thesis: ( not c in { (N . i) where i is Element of N : i >= j } or N . j <= c )
assume c in { (N . i) where i is Element of N : i >= j } ; :: thesis: N . j <= c
then consider i0 being Element of N such that
A9: c = N . i0 and
i0 >= j ;
N . j = the_value_of N by YELLOW_6:25
.= N . i0 by YELLOW_6:25 ;
hence N . j <= c by A9; :: thesis: verum

end;

for b being Element of R st b is_<=_than { (N . i) where i is Element of N : i >= j } holds
N . j >= b

proof

let c be Element of R; :: thesis: ( c is_<=_than { (N . i) where i is Element of N : i >= j } implies N . j >= c )
consider i0 being Element of N such that
A10: i0 >= j and
i0 >= j by YELLOW_6:def 5;
A11: N . i0 in { (N . i) where i is Element of N : i >= j } by A10;
assume A12: c is_<=_than { (N . i) where i is Element of N : i >= j } ; :: thesis: N . j >= c
N . j = the_value_of N by YELLOW_6:25
.= N . i0 by YELLOW_6:25 ;
hence N . j >= c by A11, A12, LATTICE3:def 8; :: thesis: verum

end;

hence N . j <= b by A7, A8, YELLOW_0:33; :: thesis: verum

end;

thus the_value_of N = N . j by YELLOW_6:25
.= lim_inf N by A1, A5, YELLOW_0:32 ; :: thesis: verum