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 object st b in f holds

b in rng the mapping of ((a_net F) | i)

for b being object st b in rng the mapping of ((a_net F) | i) holds

b in f

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 A12, A5, XBOOLE_0:def 10; :: thesis: verum

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 object st b in f holds

b in rng the mapping of ((a_net F) | i)

proof

then A5:
f c= rng the mapping of ((a_net F) | i)
;
let b be object ; :: 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) ;

[b,f] `1 = b ;

then A4: b = (a_net F) . 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 (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;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) ;

[b,f] `1 = b ;

then A4: b = (a_net F) . 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 (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

for b being object st b in rng the mapping of ((a_net F) | i) holds

b in f

proof

then A12:
rng the mapping of ((a_net F) | i) c= f
;
let b be object ; :: 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) ;

k in the carrier of (a_net F) 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 ((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;

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, A9, A10; :: thesis: verum

end;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) ;

k in the carrier of (a_net F) 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 ((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;

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, A9, A10; :: thesis: verum

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 A12, A5, XBOOLE_0:def 10; :: thesis: verum