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 (a_net F) st i `2 = f holds
inf f = inf ((a_net F) | 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 (a_net F) st i `2 = f holds
inf f = inf ((a_net F) | i)
let f be Subset of L; :: thesis: ( f in F implies for i being Element of (a_net F) st i `2 = f holds
inf f = inf ((a_net F) | i) )
assume A1: f in F ; :: thesis: for i being Element of (a_net F) st i `2 = f holds
inf f = inf ((a_net F) | i)
let i be Element of (a_net F); :: thesis: ( i `2 = f implies inf f = inf ((a_net F) | i) )
assume A2: i `2 = f ; :: thesis: inf f = inf ((a_net F) | i)
for b being set st b in f holds
b in rng the mapping of ((a_net F) | i)

proof

let b be set ; :: thesis: ( b in f implies b in rng the mapping of ((a_net F) | i) )
assume A3: b in f ; :: thesis: b in rng the mapping of ((a_net F) | 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 (a_net F) by YELLOW19:def 4;
reconsider l = k as Element of (a_net F) ;
k `1 = b by MCART_1:def 1;
then A4: b = (a_net F) . k by YELLOW19:def 4;
k `2 c= i `2 by A2, MCART_1:def 2;
then i <= k by YELLOW19:def 4;
then l in { y where y is Element of (a_net F) : i <= y } ;
then reconsider k = k as Element of ((a_net F) | i) by WAYBEL_9:12;
reconsider k = k as Element of ((a_net F) | i) ;
(a_net F) . l = ((a_net F) | i) . k by WAYBEL_9:16;
then b in { (((a_net F) | i) . m) where m is Element of ((a_net F) | i) : verum } by A4;
hence b in rng the mapping of ((a_net F) | i) by WAYBEL11:19; :: thesis: verum

end;

then A5: f c= rng the mapping of ((a_net F) | i) by TARSKI:def 3;
for b being set st b in rng the mapping of ((a_net F) | i) holds
b in f

proof

let b be set ; :: thesis: ( b in rng the mapping of ((a_net F) | i) implies b in f )
assume b in rng the mapping of ((a_net F) | i) ; :: thesis: b in f
then b in { (((a_net F) | i) . k) where k is Element of ((a_net F) | i) : verum } by WAYBEL11:19;
then consider k being Element of ((a_net F) | i) such that
A6: b = ((a_net F) | i) . k ;
A7: the carrier of ((a_net F) | i) c= the carrier of (a_net F) by WAYBEL_9:13;
then reconsider l = k as Element of (a_net F) by TARSKI:def 3;
k in the carrier of (a_net F) by A7, TARSKI:def 3;
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 ((a_net F) | i) ;
then k in { y where y is Element of (a_net F) : i <= y } by WAYBEL_9:12;
then ex y being Element of (a_net F) st
( k = y & i <= y ) ;
then A9: l `2 c= f by A2, YELLOW19:def 4;
consider c being Element of L, g being Element of F such that
A10: k = [c,g] and
A11: c in g by A8;
A12: ( k `1 = c & k `2 = g ) by A10, MCART_1:def 1, MCART_1:def 2;
reconsider k = k as Element of ((a_net F) | i) ;
(a_net F) . l = ((a_net F) | i) . k by WAYBEL_9:16;
then b = l `1 by A6, YELLOW19:def 4;
hence b in f by A11, A12, A9; :: thesis: verum

end;

then A13: rng the mapping of ((a_net F) | i) c= f by TARSKI:def 3;
inf ((a_net F) | i) = Inf by WAYBEL_9:def 2
.= "/\" (rng the mapping of ((a_net F) | i)),L by YELLOW_2:def 6 ;
hence inf f = inf ((a_net F) | i) by A13, A5, XBOOLE_0:def 10; :: thesis: verum