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

let F be ultra Filter of (BoolePoset ([#] L)); :: thesis: for p being greater_or_equal_to_id Function of (),() holds lim_inf F >= inf (() * p)
let p be greater_or_equal_to_id Function of (),(); :: thesis: lim_inf F >= inf (() * p)
set M = () * p;
set rM = rng the mapping of (() * p);
set C = the Element of F;
A1: inf (() * p) = Inf by WAYBEL_9:def 2
.= "/\" ((rng the mapping of (() * 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 (() * p)) c= [#] L by XBOOLE_1:1;
then reconsider D = the Element of F \ (rng the mapping of (() * p)), A = the Element of F /\ (rng the mapping of (() * p)) as Element of (BoolePoset ([#] L)) by WAYBEL_7:2;
A3: the carrier of (() * p) = the carrier of () by WAYBEL28:6;
then reconsider g = p as Function of (() * p),() ;
A4: now :: thesis: not D 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 ;
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 () by YELLOW19:def 4;
reconsider dD9 = dD as Element of (() * p) by WAYBEL28:6;
A8: dom p = the carrier of () by FUNCT_2:52;
ex i being Element of (() * p) st
for j being Element of (() * p) st j >= i holds
g . j >= dD
proof
consider i being Element of (() * p) such that
A9: i = dD9 ;
take i ; :: thesis: for j being Element of (() * p) st j >= i holds
g . j >= dD

for j being Element of (() * p) st j >= i holds
g . j >= dD
proof
reconsider i9 = i as Element of () by WAYBEL28:6;
let j be Element of (() * p); :: thesis: ( j >= i implies g . j >= dD )
reconsider j9 = j as Element of () by WAYBEL28:6;
A10: j9 <= g . j by WAYBEL28:def 1;
reconsider i9 = i9 as Element of () ;
reconsider j9 = j9 as Element of () ;
A11: RelStr(# the carrier of (() * p), the InternalRel of (() * p) #) = RelStr(# the carrier of (), the InternalRel of () #) by WAYBEL28:def 2;
assume j >= i ; :: thesis: g . j >= dD
then i9 <= j9 by ;
hence g . j >= dD by ; :: thesis: verum
end;
hence for j being Element of (() * p) st j >= i holds
g . j >= dD ; :: thesis: verum
end;
then consider i being Element of (() * p) such that
A12: for j being Element of (() * p) st j >= i holds
g . j >= dD ;
RelStr(# the carrier of (() * p), the InternalRel of (() * p) #) = RelStr(# the carrier of (), the InternalRel of () #) 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 ;
reconsider G = g . i as Element of () ;
g . i in the carrier of () ;
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 ;
(() * p) . i = ( the mapping of () * p) . i by WAYBEL28:def 2
.= () . G by
.= (p . i) `1 by YELLOW19:def 4 ;
then not ((a_net F) * p) . i in rng the mapping of (() * p) by ;
hence contradiction by FUNCT_2:4; :: thesis: verum
end;
set Y = { (inf B) where B is Subset of L : B in 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 ;
then inf A9 in { (inf B) where B is Subset of L : B in F } ;
then A19: inf A9 <= lim_inf F by ;
A c= rng the mapping of (() * p) by XBOOLE_1:17;
then inf (() * p) <= inf A9 by ;
hence lim_inf F >= inf (() * p) by ; :: thesis: verum