let L be complete LATTICE; :: thesis: for N being net of L holds lim_inf N = "\/" ( { (inf (N | i)) where i is Element of N : verum } ,L)

let N be net of L; :: thesis: lim_inf N = "\/" ( { (inf (N | i)) where i is Element of N : verum } ,L)

set X = { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } ;

set Y = { (inf (N | i)) where i is Element of N : verum } ;

for x being object st x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } holds

x in { (inf (N | i)) where i is Element of N : verum }

for x being object st x in { (inf (N | i)) where i is Element of N : verum } holds

x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum }

hence lim_inf N = "\/" ( { (inf (N | i)) where i is Element of N : verum } ,L) by A12, XBOOLE_0:def 10; :: thesis: verum

let N be net of L; :: thesis: lim_inf N = "\/" ( { (inf (N | i)) where i is Element of N : verum } ,L)

set X = { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } ;

set Y = { (inf (N | i)) where i is Element of N : verum } ;

for x being object st x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } holds

x in { (inf (N | i)) where i is Element of N : verum }

proof

then A12:
( lim_inf N = "\/" ( { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } ,L) & { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } c= { (inf (N | i)) where i is Element of N : verum } )
by WAYBEL11:def 6;
let x be object ; :: thesis: ( x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } implies x in { (inf (N | i)) where i is Element of N : verum } )

assume x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } ; :: thesis: x in { (inf (N | i)) where i is Element of N : verum }

then consider j being Element of N such that

A1: x = "/\" ( { (N . i) where i is Element of N : i >= j } ,L) ;

reconsider x = x as Element of L by A1;

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

reconsider i = j as Element of N ;

for b being object st b in rng the mapping of (N | i) holds

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

A5: ex_inf_of { (N . i) where i is Element of N : i >= j } ,L by YELLOW_0:17;

then A6: { (N . i) where i is Element of N : i >= j } is_>=_than x by A1, YELLOW_0:def 10;

A7: rng the mapping of (N | i) is_>=_than x by A6, A4;

for b being object st b in { (N . i) where i is Element of N : i >= j } holds

b in rng the mapping of (N | i)

then { (N . i) where i is Element of N : i >= j } = rng the mapping of (N | i) by A4;

then for a being Element of L st rng the mapping of (N | i) is_>=_than a holds

a <= x by A1, A5, YELLOW_0:def 10;

then consider i being Element of N such that

A10: ( ex_inf_of rng the mapping of (N | i),L & rng the mapping of (N | i) is_>=_than x & ( for a being Element of L st rng the mapping of (N | i) is_>=_than a holds

a <= x ) ) by A7, YELLOW_0:17;

A11: inf (N | i) = Inf by WAYBEL_9:def 2

.= "/\" ((rng the mapping of (N | i)),L) by YELLOW_2:def 6 ;

x = "/\" ((rng the mapping of (N | i)),L) by A10, YELLOW_0:def 10;

hence x in { (inf (N | i)) where i is Element of N : verum } by A11; :: thesis: verum

end;assume x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } ; :: thesis: x in { (inf (N | i)) where i is Element of N : verum }

then consider j being Element of N such that

A1: x = "/\" ( { (N . i) where i is Element of N : i >= j } ,L) ;

reconsider x = x as Element of L by A1;

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

reconsider i = j as Element of N ;

for b being object st b in rng the mapping of (N | i) holds

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

proof

then A4:
rng the mapping of (N | i) c= { (N . i) where i is Element of N : i >= j }
;
let b be object ; :: thesis: ( b in rng the mapping of (N | i) implies b in { (N . i) where i is Element of N : i >= j } )

assume b in rng the mapping of (N | i) ; :: thesis: b in { (N . i) where i is Element of N : i >= j }

then b in { ((N | i) . k) where k is Element of (N | i) : verum } by WAYBEL11:19;

then consider k being Element of (N | i) such that

A2: b = (N | i) . k ;

the carrier of (N | i) c= the carrier of N by WAYBEL_9:13;

then reconsider l = k as Element of N ;

k in the carrier of (N | i) ;

then k in { y where y is Element of N : i <= y } by WAYBEL_9:12;

then A3: ex y being Element of N st

( k = y & i <= y ) ;

reconsider k = k as Element of (N | i) ;

N . l = (N | i) . k by WAYBEL_9:16;

hence b in { (N . i) where i is Element of N : i >= j } by A2, A3; :: thesis: verum

end;assume b in rng the mapping of (N | i) ; :: thesis: b in { (N . i) where i is Element of N : i >= j }

then b in { ((N | i) . k) where k is Element of (N | i) : verum } by WAYBEL11:19;

then consider k being Element of (N | i) such that

A2: b = (N | i) . k ;

the carrier of (N | i) c= the carrier of N by WAYBEL_9:13;

then reconsider l = k as Element of N ;

k in the carrier of (N | i) ;

then k in { y where y is Element of N : i <= y } by WAYBEL_9:12;

then A3: ex y being Element of N st

( k = y & i <= y ) ;

reconsider k = k as Element of (N | i) ;

N . l = (N | i) . k by WAYBEL_9:16;

hence b in { (N . i) where i is Element of N : i >= j } by A2, A3; :: thesis: verum

A5: ex_inf_of { (N . i) where i is Element of N : i >= j } ,L by YELLOW_0:17;

then A6: { (N . i) where i is Element of N : i >= j } is_>=_than x by A1, YELLOW_0:def 10;

A7: rng the mapping of (N | i) is_>=_than x by A6, A4;

for b being object st b in { (N . i) where i is Element of N : i >= j } holds

b in rng the mapping of (N | i)

proof

then
{ (N . i) where i is Element of N : i >= j } c= rng the mapping of (N | i)
;
let b be object ; :: thesis: ( b in { (N . i) where i is Element of N : i >= j } implies b in rng the mapping of (N | i) )

assume b in { (N . i) where i is Element of N : i >= j } ; :: thesis: b in rng the mapping of (N | i)

then consider k being Element of N such that

A8: b = N . k and

A9: k >= j ;

reconsider l = k as Element of N ;

l in { y where y is Element of N : i <= y } by A9;

then reconsider k = k as Element of (N | i) by WAYBEL_9:12;

reconsider k = k as Element of (N | i) ;

N . l = (N | i) . k by WAYBEL_9:16;

then b in { ((N | i) . m) where m is Element of (N | i) : verum } by A8;

hence b in rng the mapping of (N | i) by WAYBEL11:19; :: thesis: verum

end;assume b in { (N . i) where i is Element of N : i >= j } ; :: thesis: b in rng the mapping of (N | i)

then consider k being Element of N such that

A8: b = N . k and

A9: k >= j ;

reconsider l = k as Element of N ;

l in { y where y is Element of N : i <= y } by A9;

then reconsider k = k as Element of (N | i) by WAYBEL_9:12;

reconsider k = k as Element of (N | i) ;

N . l = (N | i) . k by WAYBEL_9:16;

then b in { ((N | i) . m) where m is Element of (N | i) : verum } by A8;

hence b in rng the mapping of (N | i) by WAYBEL11:19; :: thesis: verum

then { (N . i) where i is Element of N : i >= j } = rng the mapping of (N | i) by A4;

then for a being Element of L st rng the mapping of (N | i) is_>=_than a holds

a <= x by A1, A5, YELLOW_0:def 10;

then consider i being Element of N such that

A10: ( ex_inf_of rng the mapping of (N | i),L & rng the mapping of (N | i) is_>=_than x & ( for a being Element of L st rng the mapping of (N | i) is_>=_than a holds

a <= x ) ) by A7, YELLOW_0:17;

A11: inf (N | i) = Inf by WAYBEL_9:def 2

.= "/\" ((rng the mapping of (N | i)),L) by YELLOW_2:def 6 ;

x = "/\" ((rng the mapping of (N | i)),L) by A10, YELLOW_0:def 10;

hence x in { (inf (N | i)) where i is Element of N : verum } by A11; :: thesis: verum

for x being object st x in { (inf (N | i)) where i is Element of N : verum } holds

x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum }

proof

then
{ (inf (N | i)) where i is Element of N : verum } c= { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum }
;
let x be object ; :: thesis: ( x in { (inf (N | i)) where i is Element of N : verum } implies x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } )

assume x in { (inf (N | i)) where i is Element of N : verum } ; :: thesis: x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum }

then consider i being Element of N such that

A13: x = inf (N | i) ;

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

for b being object st b in rng the mapping of (N | i) holds

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

reconsider x = x as Element of L by A13;

A17: x = Inf by A13, WAYBEL_9:def 2

.= "/\" ((rng the mapping of (N | i)),L) by YELLOW_2:def 6 ;

for b being object st b in { (N . j) where j is Element of N : j >= i } holds

b in rng the mapping of (N | i)

then rng the mapping of (N | i) = { (N . j) where j is Element of N : j >= i } by A16;

hence x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } by A17; :: thesis: verum

end;assume x in { (inf (N | i)) where i is Element of N : verum } ; :: thesis: x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum }

then consider i being Element of N such that

A13: x = inf (N | i) ;

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

for b being object st b in rng the mapping of (N | i) holds

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

proof

then A16:
rng the mapping of (N | i) c= { (N . j) where j is Element of N : j >= i }
;
let b be object ; :: thesis: ( b in rng the mapping of (N | i) implies b in { (N . j) where j is Element of N : j >= i } )

assume b in rng the mapping of (N | i) ; :: thesis: b in { (N . j) where j is Element of N : j >= i }

then b in { ((N | i) . k) where k is Element of (N | i) : verum } by WAYBEL11:19;

then consider k being Element of (N | i) such that

A14: b = (N | i) . k ;

the carrier of (N | i) c= the carrier of N by WAYBEL_9:13;

then reconsider l = k as Element of N ;

k in the carrier of (N | i) ;

then k in { y where y is Element of N : i <= y } by WAYBEL_9:12;

then A15: ex y being Element of N st

( k = y & i <= y ) ;

reconsider k = k as Element of (N | i) ;

N . l = (N | i) . k by WAYBEL_9:16;

hence b in { (N . j) where j is Element of N : j >= i } by A14, A15; :: thesis: verum

end;assume b in rng the mapping of (N | i) ; :: thesis: b in { (N . j) where j is Element of N : j >= i }

then b in { ((N | i) . k) where k is Element of (N | i) : verum } by WAYBEL11:19;

then consider k being Element of (N | i) such that

A14: b = (N | i) . k ;

the carrier of (N | i) c= the carrier of N by WAYBEL_9:13;

then reconsider l = k as Element of N ;

k in the carrier of (N | i) ;

then k in { y where y is Element of N : i <= y } by WAYBEL_9:12;

then A15: ex y being Element of N st

( k = y & i <= y ) ;

reconsider k = k as Element of (N | i) ;

N . l = (N | i) . k by WAYBEL_9:16;

hence b in { (N . j) where j is Element of N : j >= i } by A14, A15; :: thesis: verum

reconsider x = x as Element of L by A13;

A17: x = Inf by A13, WAYBEL_9:def 2

.= "/\" ((rng the mapping of (N | i)),L) by YELLOW_2:def 6 ;

for b being object st b in { (N . j) where j is Element of N : j >= i } holds

b in rng the mapping of (N | i)

proof

then
{ (N . j) where j is Element of N : j >= i } c= rng the mapping of (N | i)
;
let b be object ; :: thesis: ( b in { (N . j) where j is Element of N : j >= i } implies b in rng the mapping of (N | i) )

assume b in { (N . j) where j is Element of N : j >= i } ; :: thesis: b in rng the mapping of (N | i)

then consider k being Element of N such that

A18: b = N . k and

A19: k >= i ;

reconsider l = k as Element of N ;

l in { y where y is Element of N : i <= y } by A19;

then reconsider k = k as Element of (N | i) by WAYBEL_9:12;

reconsider k = k as Element of (N | i) ;

N . l = (N | i) . k by WAYBEL_9:16;

then b in { ((N | i) . m) where m is Element of (N | i) : verum } by A18;

hence b in rng the mapping of (N | i) by WAYBEL11:19; :: thesis: verum

end;assume b in { (N . j) where j is Element of N : j >= i } ; :: thesis: b in rng the mapping of (N | i)

then consider k being Element of N such that

A18: b = N . k and

A19: k >= i ;

reconsider l = k as Element of N ;

l in { y where y is Element of N : i <= y } by A19;

then reconsider k = k as Element of (N | i) by WAYBEL_9:12;

reconsider k = k as Element of (N | i) ;

N . l = (N | i) . k by WAYBEL_9:16;

then b in { ((N | i) . m) where m is Element of (N | i) : verum } by A18;

hence b in rng the mapping of (N | i) by WAYBEL11:19; :: thesis: verum

then rng the mapping of (N | i) = { (N . j) where j is Element of N : j >= i } by A16;

hence x in { ("/\" ( { (N . i) where i is Element of N : i >= j } ,L)) where j is Element of N : verum } by A17; :: thesis: verum

hence lim_inf N = "\/" ( { (inf (N | i)) where i is Element of N : verum } ,L) by A12, XBOOLE_0:def 10; :: thesis: verum