let L be complete LATTICE; :: thesis: for F being proper Filter of (BoolePoset ([#] L)) holds lim_inf F = lim_inf (a_net F)

let F be proper Filter of (BoolePoset ([#] L)); :: thesis: lim_inf F = lim_inf (a_net F)

set X = { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum } ;

set Y = { (inf B) where B is Subset of L : B in F } ;

for x being object st x in { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum } holds

x in { (inf B) where B is Subset of L : B in F }

for x being object st x in { (inf B) where B is Subset of L : B in F } holds

x in { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum }

lim_inf (a_net F) = "\/" ( { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum } ,L) by Th11;

hence lim_inf F = lim_inf (a_net F) by A3, A7, XBOOLE_0:def 10; :: thesis: verum

let F be proper Filter of (BoolePoset ([#] L)); :: thesis: lim_inf F = lim_inf (a_net F)

set X = { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum } ;

set Y = { (inf B) where B is Subset of L : B in F } ;

for x being object st x in { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum } holds

x in { (inf B) where B is Subset of L : B in F }

proof

then A3:
{ (inf ((a_net F) | i)) where i is Element of (a_net F) : verum } c= { (inf B) where B is Subset of L : B in F }
;
let x be object ; :: thesis: ( x in { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum } implies x in { (inf B) where B is Subset of L : B in F } )

assume x in { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum } ; :: thesis: x in { (inf B) where B is Subset of L : B in F }

then consider i being Element of (a_net F) such that

A1: x = inf ((a_net F) | i) ;

reconsider i = i as Element of (a_net F) ;

i in the carrier of (a_net F) ;

then i in { [b,g] where b is Element of L, g is Element of F : b in g } by YELLOW19:def 4;

then consider a being Element of L, f being Element of F such that

A2: i = [a,f] and

a in f ;

reconsider i = i as Element of (a_net F) ;

reconsider f = f as Element of (BoolePoset ([#] L)) ;

reconsider f = f as Subset of L by WAYBEL_7:2;

[a,f] `2 = f ;

then inf f = inf ((a_net F) | i) by Th12, A2;

hence x in { (inf B) where B is Subset of L : B in F } by A1; :: thesis: verum

end;assume x in { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum } ; :: thesis: x in { (inf B) where B is Subset of L : B in F }

then consider i being Element of (a_net F) such that

A1: x = inf ((a_net F) | i) ;

reconsider i = i as Element of (a_net F) ;

i in the carrier of (a_net F) ;

then i in { [b,g] where b is Element of L, g is Element of F : b in g } by YELLOW19:def 4;

then consider a being Element of L, f being Element of F such that

A2: i = [a,f] and

a in f ;

reconsider i = i as Element of (a_net F) ;

reconsider f = f as Element of (BoolePoset ([#] L)) ;

reconsider f = f as Subset of L by WAYBEL_7:2;

[a,f] `2 = f ;

then inf f = inf ((a_net F) | i) by Th12, A2;

hence x in { (inf B) where B is Subset of L : B in F } by A1; :: thesis: verum

for x being object st x in { (inf B) where B is Subset of L : B in F } holds

x in { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum }

proof

then A7:
{ (inf B) where B is Subset of L : B in F } c= { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum }
;
let x be object ; :: thesis: ( x in { (inf B) where B is Subset of L : B in F } implies x in { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum } )

assume x in { (inf B) where B is Subset of L : B in F } ; :: thesis: x in { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum }

then consider B being Subset of L such that

A4: x = inf B and

A5: B in F ;

not Bottom (BoolePoset ([#] L)) in F by WAYBEL_7:4;

then B <> {} by A5, YELLOW_1:18;

then consider a being Element of L such that

A6: a in B by SUBSET_1:4;

reconsider B = B as Element of F by A5;

[a,B] in { [b,f] where b is Element of L, f is Element of F : b in f } by A6;

then reconsider i = [a,B] as Element of (a_net F) by YELLOW19:def 4;

[a,B] `2 = B ;

then x = inf ((a_net F) | i) by A4, Th12;

hence x in { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum } ; :: thesis: verum

end;assume x in { (inf B) where B is Subset of L : B in F } ; :: thesis: x in { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum }

then consider B being Subset of L such that

A4: x = inf B and

A5: B in F ;

not Bottom (BoolePoset ([#] L)) in F by WAYBEL_7:4;

then B <> {} by A5, YELLOW_1:18;

then consider a being Element of L such that

A6: a in B by SUBSET_1:4;

reconsider B = B as Element of F by A5;

[a,B] in { [b,f] where b is Element of L, f is Element of F : b in f } by A6;

then reconsider i = [a,B] as Element of (a_net F) by YELLOW19:def 4;

[a,B] `2 = B ;

then x = inf ((a_net F) | i) by A4, Th12;

hence x in { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum } ; :: thesis: verum

lim_inf (a_net F) = "\/" ( { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum } ,L) by Th11;

hence lim_inf F = lim_inf (a_net F) by A3, A7, XBOOLE_0:def 10; :: thesis: verum