let L be complete LATTICE; :: thesis: for F being proper Filter of (BoolePoset ([#] L))
for f being Subset of L st f in F holds
for i being Element of () st i `2 = f holds
inf f = inf (() | i)

let F be proper Filter of (BoolePoset ([#] L)); :: thesis: for f being Subset of L st f in F holds
for i being Element of () st i `2 = f holds
inf f = inf (() | i)

let f be Subset of L; :: thesis: ( f in F implies for i being Element of () st i `2 = f holds
inf f = inf (() | i) )

assume A1: f in F ; :: thesis: for i being Element of () st i `2 = f holds
inf f = inf (() | i)

let i be Element of (); :: thesis: ( i `2 = f implies inf f = inf (() | i) )
assume A2: i `2 = f ; :: thesis: inf f = inf (() | i)
for b being object st b in f holds
b in rng the mapping of (() | i)
proof
let b be object ; :: thesis: ( b in f implies b in rng the mapping of (() | i) )
assume A3: b in f ; :: thesis: b in rng the mapping of (() | i)
then reconsider b = b as Element of L ;
reconsider f = f as Element of F by A1;
[b,f] in { [a,g] where a is Element of L, g is Element of F : a in g } by A3;
then reconsider k = [b,f] as Element of () by YELLOW19:def 4;
reconsider l = k as Element of () ;
[b,f] `1 = b ;
then A4: b = () . k by YELLOW19:def 4;
k `2 c= i `2 by A2;
then i <= k by YELLOW19:def 4;
then l in { y where y is Element of () : i <= y } ;
then reconsider k = k as Element of (() | i) by WAYBEL_9:12;
reconsider k = k as Element of (() | i) ;
(a_net F) . l = (() | i) . k by WAYBEL_9:16;
then b in { ((() | i) . m) where m is Element of (() | i) : verum } by A4;
hence b in rng the mapping of (() | i) by WAYBEL11:19; :: thesis: verum
end;
then A5: f c= rng the mapping of (() | i) ;
for b being object st b in rng the mapping of (() | i) holds
b in f
proof
let b be object ; :: thesis: ( b in rng the mapping of (() | i) implies b in f )
assume b in rng the mapping of (() | i) ; :: thesis: b in f
then b in { ((() | i) . k) where k is Element of (() | i) : verum } by WAYBEL11:19;
then consider k being Element of (() | i) such that
A6: b = (() | i) . k ;
A7: the carrier of (() | i) c= the carrier of () by WAYBEL_9:13;
then reconsider l = k as Element of () ;
k in the carrier of () by A7;
then A8: k in { [c,g] where c is Element of L, g is Element of F : c in g } by YELLOW19:def 4;
k in the carrier of (() | i) ;
then k in { y where y is Element of () : i <= y } by WAYBEL_9:12;
then ex y being Element of () st
( k = y & i <= y ) ;
then A9: l `2 c= f by ;
consider c being Element of L, g being Element of F such that
A10: k = [c,g] and
A11: c in g by A8;
reconsider k = k as Element of (() | i) ;
(a_net F) . l = (() | i) . k by WAYBEL_9:16;
then b = l `1 by ;
hence b in f by A11, A9, A10; :: thesis: verum
end;
then A12: rng the mapping of (() | i) c= f ;
inf (() | i) = Inf by WAYBEL_9:def 2
.= "/\" ((rng the mapping of (() | i)),L) by YELLOW_2:def 6 ;
hence inf f = inf (() | i) by ; :: thesis: verum