let L be complete LATTICE; 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)); 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); 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 not D in Fset d = the
Element of
D;
assume A5:
D in F
;
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
then consider i being
Element of
((a_net F) * p) such that 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;
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 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; verum