let L be complete LATTICE; :: thesis: for F being ultra Filter of (BoolePoset ([#] L))

for p being greater_or_equal_to_id Function of (a_net F),(a_net F) holds lim_inf F >= inf ((a_net F) * p)

let F be ultra Filter of (BoolePoset ([#] L)); :: thesis: for p being greater_or_equal_to_id Function of (a_net F),(a_net F) holds lim_inf F >= inf ((a_net F) * p)

let p be greater_or_equal_to_id Function of (a_net F),(a_net F); :: thesis: lim_inf F >= inf ((a_net F) * p)

set M = (a_net F) * p;

set rM = rng the mapping of ((a_net F) * p);

set C = the Element of F;

A1: inf ((a_net F) * p) = Inf by WAYBEL_9:def 2

.= "/\" ((rng the mapping of ((a_net F) * p)),L) by YELLOW_2:def 6 ;

F c= the carrier of (BoolePoset ([#] L)) ;

then F c= bool ([#] L) by WAYBEL_7:2;

then the Element of F in bool ([#] L) ;

then A2: the Element of F \ (rng the mapping of ((a_net F) * p)) c= [#] L by XBOOLE_1:1;

then reconsider D = the Element of F \ (rng the mapping of ((a_net F) * p)), A = the Element of F /\ (rng the mapping of ((a_net F) * p)) as Element of (BoolePoset ([#] L)) by WAYBEL_7:2;

A3: the carrier of ((a_net F) * p) = the carrier of (a_net F) by WAYBEL28:6;

then reconsider g = p as Function of ((a_net F) * p),(a_net F) ;

reconsider A9 = A as Subset of L ;

A18: D "\/" A = D \/ A by YELLOW_1:17

.= the Element of F by XBOOLE_1:51 ;

F is prime by WAYBEL_7:22;

then A in F by A18, A4;

then inf A9 in { (inf B) where B is Subset of L : B in F } ;

then A19: inf A9 <= lim_inf F by YELLOW_0:17, YELLOW_4:1;

A c= rng the mapping of ((a_net F) * p) by XBOOLE_1:17;

then inf ((a_net F) * p) <= inf A9 by A1, WAYBEL_7:1;

hence lim_inf F >= inf ((a_net F) * p) by A19, YELLOW_0:def 2; :: thesis: verum

for p being greater_or_equal_to_id Function of (a_net F),(a_net F) holds lim_inf F >= inf ((a_net F) * p)

let F be ultra Filter of (BoolePoset ([#] L)); :: thesis: for p being greater_or_equal_to_id Function of (a_net F),(a_net F) holds lim_inf F >= inf ((a_net F) * p)

let p be greater_or_equal_to_id Function of (a_net F),(a_net F); :: thesis: lim_inf F >= inf ((a_net F) * p)

set M = (a_net F) * p;

set rM = rng the mapping of ((a_net F) * p);

set C = the Element of F;

A1: inf ((a_net F) * p) = Inf by WAYBEL_9:def 2

.= "/\" ((rng the mapping of ((a_net F) * p)),L) by YELLOW_2:def 6 ;

F c= the carrier of (BoolePoset ([#] L)) ;

then F c= bool ([#] L) by WAYBEL_7:2;

then the Element of F in bool ([#] L) ;

then A2: the Element of F \ (rng the mapping of ((a_net F) * p)) c= [#] L by XBOOLE_1:1;

then reconsider D = the Element of F \ (rng the mapping of ((a_net F) * p)), A = the Element of F /\ (rng the mapping of ((a_net F) * p)) as Element of (BoolePoset ([#] L)) by WAYBEL_7:2;

A3: the carrier of ((a_net F) * p) = the carrier of (a_net F) by WAYBEL28:6;

then reconsider g = p as Function of ((a_net F) * p),(a_net F) ;

A4: now :: thesis: not D in F

set Y = { (inf B) where B is Subset of L : B in F } ;set d = the Element of D;

assume A5: D in F ; :: thesis: contradiction

not Bottom (BoolePoset ([#] L)) in F by WAYBEL_7:4;

then A6: D <> {} by A5, YELLOW_1:18;

then A7: the Element of D in D ;

reconsider D = D as Element of F by A5;

reconsider d = the Element of D as Element of L by A2, A7;

[d,D] in { [a,f] where a is Element of L, f is Element of F : a in f } by A6;

then reconsider dD = [d,D] as Element of (a_net F) by YELLOW19:def 4;

reconsider dD9 = dD as Element of ((a_net F) * p) by WAYBEL28:6;

A8: dom p = the carrier of (a_net F) by FUNCT_2:52;

ex i being Element of ((a_net F) * p) st

for j being Element of ((a_net F) * p) st j >= i holds

g . j >= dD

A12: for j being Element of ((a_net F) * p) st j >= i holds

g . j >= dD ;

RelStr(# the carrier of ((a_net F) * p), the InternalRel of ((a_net F) * p) #) = RelStr(# the carrier of (a_net F), the InternalRel of (a_net F) #) by WAYBEL28:def 2;

then (a_net F) * p is reflexive by WAYBEL_8:12;

then i >= i by YELLOW_0:def 1;

then A13: g . i >= dD by A12;

[d,D] `2 = D ;

then A14: (p . i) `2 c= D by A13, YELLOW19:def 4;

reconsider G = g . i as Element of (a_net F) ;

g . i in the carrier of (a_net F) ;

then g . i in { [a,f] where a is Element of L, f is Element of F : a in f } by YELLOW19:def 4;

then consider a being Element of L, f being Element of F such that

A15: g . i = [a,f] and

A16: a in f ;

A17: (p . i) `1 in (p . i) `2 by A15, A16;

((a_net F) * p) . i = ( the mapping of (a_net F) * p) . i by WAYBEL28:def 2

.= (a_net F) . G by A3, A8, FUNCT_1:13

.= (p . i) `1 by YELLOW19:def 4 ;

then not ((a_net F) * p) . i in rng the mapping of ((a_net F) * p) by A14, A17, XBOOLE_0:def 5;

hence contradiction by FUNCT_2:4; :: thesis: verum

end;assume A5: D in F ; :: thesis: contradiction

not Bottom (BoolePoset ([#] L)) in F by WAYBEL_7:4;

then A6: D <> {} by A5, YELLOW_1:18;

then A7: the Element of D in D ;

reconsider D = D as Element of F by A5;

reconsider d = the Element of D as Element of L by A2, A7;

[d,D] in { [a,f] where a is Element of L, f is Element of F : a in f } by A6;

then reconsider dD = [d,D] as Element of (a_net F) by YELLOW19:def 4;

reconsider dD9 = dD as Element of ((a_net F) * p) by WAYBEL28:6;

A8: dom p = the carrier of (a_net F) by FUNCT_2:52;

ex i being Element of ((a_net F) * p) st

for j being Element of ((a_net F) * p) st j >= i holds

g . j >= dD

proof

then consider i being Element of ((a_net F) * p) such that
consider i being Element of ((a_net F) * p) such that

A9: i = dD9 ;

take i ; :: thesis: for j being Element of ((a_net F) * p) st j >= i holds

g . j >= dD

for j being Element of ((a_net F) * p) st j >= i holds

g . j >= dD

g . j >= dD ; :: thesis: verum

end;A9: i = dD9 ;

take i ; :: thesis: for j being Element of ((a_net F) * p) st j >= i holds

g . j >= dD

for j being Element of ((a_net F) * p) st j >= i holds

g . j >= dD

proof

hence
for j being Element of ((a_net F) * p) st j >= i holds
reconsider i9 = i as Element of (a_net F) by WAYBEL28:6;

let j be Element of ((a_net F) * p); :: thesis: ( j >= i implies g . j >= dD )

reconsider j9 = j as Element of (a_net F) by WAYBEL28:6;

A10: j9 <= g . j by WAYBEL28:def 1;

reconsider i9 = i9 as Element of (a_net F) ;

reconsider j9 = j9 as Element of (a_net F) ;

A11: RelStr(# the carrier of ((a_net F) * p), the InternalRel of ((a_net F) * p) #) = RelStr(# the carrier of (a_net F), the InternalRel of (a_net F) #) by WAYBEL28:def 2;

assume j >= i ; :: thesis: g . j >= dD

then i9 <= j9 by A11, YELLOW_0:1;

hence g . j >= dD by A9, A10, YELLOW_0:def 2; :: thesis: verum

end;let j be Element of ((a_net F) * p); :: thesis: ( j >= i implies g . j >= dD )

reconsider j9 = j as Element of (a_net F) by WAYBEL28:6;

A10: j9 <= g . j by WAYBEL28:def 1;

reconsider i9 = i9 as Element of (a_net F) ;

reconsider j9 = j9 as Element of (a_net F) ;

A11: RelStr(# the carrier of ((a_net F) * p), the InternalRel of ((a_net F) * p) #) = RelStr(# the carrier of (a_net F), the InternalRel of (a_net F) #) by WAYBEL28:def 2;

assume j >= i ; :: thesis: g . j >= dD

then i9 <= j9 by A11, YELLOW_0:1;

hence g . j >= dD by A9, A10, YELLOW_0:def 2; :: thesis: verum

g . j >= dD ; :: thesis: verum

A12: for j being Element of ((a_net F) * p) st j >= i holds

g . j >= dD ;

RelStr(# the carrier of ((a_net F) * p), the InternalRel of ((a_net F) * p) #) = RelStr(# the carrier of (a_net F), the InternalRel of (a_net F) #) by WAYBEL28:def 2;

then (a_net F) * p is reflexive by WAYBEL_8:12;

then i >= i by YELLOW_0:def 1;

then A13: g . i >= dD by A12;

[d,D] `2 = D ;

then A14: (p . i) `2 c= D by A13, YELLOW19:def 4;

reconsider G = g . i as Element of (a_net F) ;

g . i in the carrier of (a_net F) ;

then g . i in { [a,f] where a is Element of L, f is Element of F : a in f } by YELLOW19:def 4;

then consider a being Element of L, f being Element of F such that

A15: g . i = [a,f] and

A16: a in f ;

A17: (p . i) `1 in (p . i) `2 by A15, A16;

((a_net F) * p) . i = ( the mapping of (a_net F) * p) . i by WAYBEL28:def 2

.= (a_net F) . G by A3, A8, FUNCT_1:13

.= (p . i) `1 by YELLOW19:def 4 ;

then not ((a_net F) * p) . i in rng the mapping of ((a_net F) * p) by A14, A17, XBOOLE_0:def 5;

hence contradiction by FUNCT_2:4; :: thesis: verum

reconsider A9 = A as Subset of L ;

A18: D "\/" A = D \/ A by YELLOW_1:17

.= the Element of F by XBOOLE_1:51 ;

F is prime by WAYBEL_7:22;

then A in F by A18, A4;

then inf A9 in { (inf B) where B is Subset of L : B in F } ;

then A19: inf A9 <= lim_inf F by YELLOW_0:17, YELLOW_4:1;

A c= rng the mapping of ((a_net F) * p) by XBOOLE_1:17;

then inf ((a_net F) * p) <= inf A9 by A1, WAYBEL_7:1;

hence lim_inf F >= inf ((a_net F) * p) by A19, YELLOW_0:def 2; :: thesis: verum