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 }

proof

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;

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 } ;
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

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;

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 } ;
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