let T be non empty 1-sorted ; :: thesis: for F being Filter of (BoolePoset ([#] T)) holds F \ {{} } = a_filter (a_net F)
let F be Filter of (BoolePoset ([#] T)); :: thesis: F \ {{} } = a_filter (a_net F)
A1: BoolePoset ([#] T) = InclPoset (bool ([#] T)) by YELLOW_1:4;
then A2: the carrier of (BoolePoset ([#] T)) = bool ([#] T) by YELLOW_1:1;
set X = a_filter (a_net F);
A4: the carrier of (a_net F) = { [a,f] where a is Element of T, f is Element of F : a in f } by Def4;
thus F \ {{} } c= a_filter (a_net F) :: according to XBOOLE_0:def 10 :: thesis: a_filter (a_net F) c= F \ {{} }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in F \ {{} } or x in a_filter (a_net F) )
assume A5: x in F \ {{} } ; :: thesis: x in a_filter (a_net F)
then A6: ( x in F & not x in {{} } ) by XBOOLE_0:def 5;
reconsider A = x as Subset of T by A1, A5, YELLOW_1:1;
consider a being Element of A;
A7: A <> {} by A6, TARSKI:def 1;
then a in A ;
then reconsider a = a as Element of T ;
[a,A] in the carrier of (a_net F) by A4, A6, A7;
then reconsider i = [a,A] as Element of (a_net F) ;
a_net F is_eventually_in A

proof

take i ; :: according to WAYBEL_0:def 11 :: thesis: for b₁ being Element of the carrier of (a_net F) holds
( not i <= b₁ or (a_net F) . b₁ in A )
let j be Element of (a_net F); :: thesis: ( not i <= j or (a_net F) . j in A )
j in the carrier of (a_net F) ;
then consider a being Element of T, f being Element of F such that
A8: ( j = [a,f] & a in f ) by A4;
assume i <= j ; :: thesis: (a_net F) . j in A
then A9: ( j `2 c= i `2 & (a_net F) . j = j `1 ) by Def4;
( j `2 = f & i `2 = A & j `1 = a ) by A8, MCART_1:7;
hence (a_net F) . j in A by A8, A9; :: thesis: verum

end;

hence x in a_filter (a_net F) ; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in a_filter (a_net F) or x in F \ {{} } )
assume x in a_filter (a_net F) ; :: thesis: x in F \ {{} }
then A10: ( a_net F is_eventually_in x & x is Subset of T ) by Th11;
then consider i being Element of (a_net F) such that
A11: for j being Element of (a_net F) st i <= j holds
(a_net F) . j in x by WAYBEL_0:def 11;
i in the carrier of (a_net F) ;
then consider a being Element of T, f being Element of F such that
A12: ( i = [a,f] & a in f ) by A4;
A13: f c= x

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in f or x in x )
assume A14: x in f ; :: thesis: x in x
then reconsider b = x as Element of T by A2;
[b,f] in the carrier of (a_net F) by A4, A14;
then reconsider j = [b,f] as Element of (a_net F) ;
( j `2 = f & i `2 = f & j `1 = b ) by A12, MCART_1:7;
then ( i <= j & (a_net F) . j = b ) by Def4;
hence x in x by A11; :: thesis: verum

end;

then A15: ( x in F & a in x ) by A10, A12, WAYBEL_7:11;
not x in {{} } by A12, A13, TARSKI:def 1;
hence x in F \ {{} } by A15, XBOOLE_0:def 5; :: thesis: verum