let T be complete LATTICE; for N being net of T
for M being subnet of N holds lim_inf N <= lim_inf M
let N be net of T; for M being subnet of N holds lim_inf N <= lim_inf M
let M be subnet of N; lim_inf N <= lim_inf M
deffunc H1( net of T) -> set = { ("/\" ( { ($1 . i) where i is Element of $1 : i >= j } ,T)) where j is Element of $1 : verum } ;
A1:
"\/" (H1(M),T) is_>=_than H1(N)
proof
let t be
Element of
T;
LATTICE3:def 9 ( not t in H1(N) or t <= "\/" (H1(M),T) )
assume
t in H1(
N)
;
t <= "\/" (H1(M),T)
then consider j being
Element of
N such that A2:
t = "/\" (
{ (N . i) where i is Element of N : i >= j } ,
T)
;
set e = the
Embedding of
M,
N;
reconsider j =
j as
Element of
N ;
consider j9 being
Element of
M such that A3:
for
p being
Element of
M st
j9 <= p holds
j <= the
Embedding of
M,
N . p
by Def3;
set X =
{ (N . i) where i is Element of N : i >= j } ;
set Y =
{ (M . i) where i is Element of M : i >= j9 } ;
A4:
ex_inf_of { (N . i) where i is Element of N : i >= j } ,
T
by YELLOW_0:17;
A5:
ex_inf_of { (M . i) where i is Element of M : i >= j9 } ,
T
by YELLOW_0:17;
{ (M . i) where i is Element of M : i >= j9 } c= { (N . i) where i is Element of N : i >= j }
then A8:
t <= "/\" (
{ (M . i) where i is Element of M : i >= j9 } ,
T)
by A2, A4, A5, YELLOW_0:35;
"/\" (
{ (M . i) where i is Element of M : i >= j9 } ,
T)
in H1(
M)
;
then
"/\" (
{ (M . i) where i is Element of M : i >= j9 } ,
T)
<= "\/" (
H1(
M),
T)
by YELLOW_2:22;
hence
t <= "\/" (
H1(
M),
T)
by A8, YELLOW_0:def 2;
verum
end;
A9:
lim_inf M = "\/" (H1(M),T)
by WAYBEL11:def 6;
lim_inf N = "\/" (H1(N),T)
by WAYBEL11:def 6;
hence
lim_inf N <= lim_inf M
by A1, A9, YELLOW_0:32; verum