let L be complete LATTICE; :: thesis: lim_inf-Convergence L is (CONSTANTS)

let N be constant net of L; :: according to YELLOW_6:def 20 :: thesis: ( not N in NetUniv L or [N,(the_value_of N)] in lim_inf-Convergence L )

A1: for M being subnet of N holds the_value_of N = lim_inf M

hence [N,(the_value_of N)] in lim_inf-Convergence L by A1, Def3; :: thesis: verum

let N be constant net of L; :: according to YELLOW_6:def 20 :: thesis: ( not N in NetUniv L or [N,(the_value_of N)] in lim_inf-Convergence L )

A1: for M being subnet of N holds the_value_of N = lim_inf M

proof

assume
N in NetUniv L
; :: thesis: [N,(the_value_of N)] in lim_inf-Convergence L
let M be subnet of N; :: thesis: the_value_of N = lim_inf M

A2: M is constant by Th16;

thus the_value_of N = the_value_of M by Th16

.= lim_inf M by A2, WAYBEL11:23 ; :: thesis: verum

end;A2: M is constant by Th16;

thus the_value_of N = the_value_of M by Th16

.= lim_inf M by A2, WAYBEL11:23 ; :: thesis: verum

hence [N,(the_value_of N)] in lim_inf-Convergence L by A1, Def3; :: thesis: verum