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 } ;
set j = the Element of N;
A1: N . the Element of N 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 . the Element of N )
assume b in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } ; :: thesis: b <= N . the Element of N
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 3;
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:16
.= N . the Element of N by YELLOW_6:16 ;
hence b <= N . the Element of N by A2, A4, YELLOW_2:22; :: 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 . the Element of N <= 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 . the Element of N <= b )
set Y = { (N . i) where i is Element of N : i >= the Element of N } ;
A6: "/\" ( { (N . i) where i is Element of N : i >= the Element of N } ,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 . the Element of N <= b
then A7: b >= "/\" ( { (N . i) where i is Element of N : i >= the Element of N } ,R) by A6;
A8: N . the Element of N is_<=_than { (N . i) where i is Element of N : i >= the Element of N }
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 >= the Element of N } or N . the Element of N <= c )
assume c in { (N . i) where i is Element of N : i >= the Element of N } ; :: thesis: N . the Element of N <= c
then consider i0 being Element of N such that
A9: c = N . i0 and
i0 >= the Element of N ;
N . the Element of N = the_value_of N by YELLOW_6:16
.= N . i0 by YELLOW_6:16 ;
hence N . the Element of N <= 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 >= the Element of N } holds
N . the Element of N >= b
proof
let c be Element of R; :: thesis: ( c is_<=_than { (N . i) where i is Element of N : i >= the Element of N } implies N . the Element of N >= c )
consider i0 being Element of N such that
A10: i0 >= the Element of N and
i0 >= the Element of N by YELLOW_6:def 3;
A11: N . i0 in { (N . i) where i is Element of N : i >= the Element of N } by A10;
assume A12: c is_<=_than { (N . i) where i is Element of N : i >= the Element of N } ; :: thesis: N . the Element of N >= c
N . the Element of N = the_value_of N by YELLOW_6:16
.= N . i0 by YELLOW_6:16 ;
hence N . the Element of N >= c by A11, A12; :: thesis: verum
end;
hence N . the Element of N <= b by A7, A8, YELLOW_0:33; :: thesis: verum
end;
thus the_value_of N = N . the Element of N by YELLOW_6:16
.= lim_inf N by A1, A5, YELLOW_0:32 ; :: thesis: verum