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 } ;
A1: lim_inf (a_net F) = "\/" { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum } ,L by Th11;
for x being set 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 set ; :: 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
A2: 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
A3: ( i = [a,f] & a in f ) ;
reconsider f = f as Element of (BoolePoset ([#] L)) ;
reconsider f = f as Subset of L by WAYBEL_7:4;
reconsider i = i as Element of (a_net F) ;
i `2 = f by A3, MCART_1:def 2;
then inf f = inf ((a_net F) | i) by Th12;
hence x in { (inf B) where B is Subset of L : B in F } by A2; :: thesis: verum

end;

then A4: { (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 } by TARSKI:def 3;
for x being set 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 set ; :: 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
A5: ( x = inf B & B in F ) ;
not Bottom (BoolePoset ([#] L)) in F by WAYBEL_7:8;
then B <> {} by A5, YELLOW_1:18;
then consider a being Element of L such that
A6: a in B by SUBSET_1:10;
reconsider B = B as Element of F by A5;
reconsider a = a as Element of L ;
[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;
i `2 = B by MCART_1:def 2;
then x = inf ((a_net F) | i) by A5, Th12;
hence x in { (inf ((a_net F) | i)) where i is Element of (a_net F) : verum } ; :: thesis: verum
thus verum ; :: thesis: verum

end;

then { (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 } by TARSKI:def 3;
hence lim_inf F = lim_inf (a_net F) by A1, A4, XBOOLE_0:def 10; :: thesis: verum