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)
set X = a_filter (a_net F);
A1: the carrier of (a_net F) = { [a,f] where a is Element of T, f is Element of F : a in f } by Def4;
A2: BoolePoset ([#] T) = InclPoset (bool ([#] T)) by YELLOW_1:4;
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 A3: x in F \ {{}} ; :: thesis: x in a_filter (a_net F)
then reconsider A = x as Subset of T by A2, YELLOW_1:1;
set a = the Element of A;
not x in {{}} by A3, XBOOLE_0:def 5;
then A4: A <> {} by TARSKI:def 1;
then the Element of A in A ;
then reconsider a = the Element of A as Element of T ;
x in F by A3, XBOOLE_0:def 5;
then [a,A] in the carrier of (a_net F) by A1, A4;
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 )
A5: i `2 = A by MCART_1:7;
A6: (a_net F) . j = j `1 by Def4;
assume i <= j ; :: thesis: (a_net F) . j in A
then A7: j `2 c= i `2 by Def4;
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] and
A9: a in f by A1;
A10: j `1 = a by A8, MCART_1:7;
j `2 = f by A8, MCART_1:7;
hence (a_net F) . j in A by A9, A7, A6, A5, A10; :: 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 A11: x in a_filter (a_net F) ; :: thesis: x in F \ {{}}
then a_net F is_eventually_in x by Th11;
then consider i being Element of (a_net F) such that
A12: 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
A13: i = [a,f] and
A14: a in f by A1;
A15: the carrier of (BoolePoset ([#] T)) = bool ([#] T) by A2, YELLOW_1:1;
A16: f c= x

proof

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

end;

x is Subset of T by A11, Th11;
then A20: x in F by A16, WAYBEL_7:7;
not x in {{}} by A14, A16, TARSKI:def 1;
hence x in F \ {{}} by A20, XBOOLE_0:def 5; :: thesis: verum