let R be up-complete LATTICE; :: thesis: for N being reflexive monotone net of R holds lim_inf N = sup N

let N be reflexive monotone net of R; :: thesis: lim_inf N = sup N

defpred S_{1}[ set ] means verum;

deffunc H_{1}( Element of N) -> Element of the carrier of R = N . $1;

deffunc H_{2}( Element of N) -> Element of the carrier of R = "/\" ( { (N . i) where i is Element of N : i >= $1 } ,R);

A1: for j being Element of N holds H_{1}(j) = H_{2}(j)
_{1}(j) where j is Element of N : S_{1}[j] }
by WAYBEL11:19

.= { H_{2}(j) where j is Element of N : S_{1}[j] }
from FRAENKEL:sch 5(A1)
;

hence lim_inf N = Sup by YELLOW_2:def 5

.= sup N by WAYBEL_2:def 1 ;

:: thesis: verum

let N be reflexive monotone net of R; :: thesis: lim_inf N = sup N

defpred S

deffunc H

deffunc H

A1: for j being Element of N holds H

proof

rng the mapping of N =
{ H
let j be Element of N; :: thesis: H_{1}(j) = H_{2}(j)

set Y = { (N . i) where i is Element of N : i >= j } ;

A2: N . j is_<=_than { (N . i) where i is Element of N : i >= j }

N . j >= b_{1}(j) = H_{2}(j)
by A2, YELLOW_0:31; :: thesis: verum

end;set Y = { (N . i) where i is Element of N : i >= j } ;

A2: N . j is_<=_than { (N . i) where i is Element of N : i >= j }

proof

for b being Element of R st b is_<=_than { (N . i) where i is Element of N : i >= j } holds
let y be Element of R; :: according to LATTICE3:def 8 :: thesis: ( not y in { (N . i) where i is Element of N : i >= j } or N . j <= y )

assume y in { (N . i) where i is Element of N : i >= j } ; :: thesis: N . j <= y

then ex i being Element of N st

( y = N . i & j <= i ) ;

hence N . j <= y by WAYBEL11:def 9; :: thesis: verum

end;assume y in { (N . i) where i is Element of N : i >= j } ; :: thesis: N . j <= y

then ex i being Element of N st

( y = N . i & j <= i ) ;

hence N . j <= y by WAYBEL11:def 9; :: thesis: verum

N . j >= b

proof

hence
H
let b be Element of R; :: thesis: ( b is_<=_than { (N . i) where i is Element of N : i >= j } implies N . j >= b )

assume A3: b is_<=_than { (N . i) where i is Element of N : i >= j } ; :: thesis: N . j >= b

reconsider j9 = j as Element of N ;

j9 <= j9 ;

then N . j9 in { (N . i) where i is Element of N : i >= j } ;

hence N . j >= b by A3; :: thesis: verum

end;assume A3: b is_<=_than { (N . i) where i is Element of N : i >= j } ; :: thesis: N . j >= b

reconsider j9 = j as Element of N ;

j9 <= j9 ;

then N . j9 in { (N . i) where i is Element of N : i >= j } ;

hence N . j >= b by A3; :: thesis: verum

.= { H

hence lim_inf N = Sup by YELLOW_2:def 5

.= sup N by WAYBEL_2:def 1 ;

:: thesis: verum