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 object ; :: 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 b1 being Element of the carrier of (a_net F) holds
( not i <= b1 or (a_net F) . b1 in A )
let j be Element of (a_net F); :: thesis: ( not i <= j or (a_net F) . j in A )
A5: (a_net F) . j = j `1 by Def4;
assume i <= j ; :: thesis: (a_net F) . j in A
then A6: 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
A7: j = [a,f] and
A8: a in f by A1;
A9: j `1 = a by A7;
j `2 = f by A7;
hence (a_net F) . j in A by A8, A6, A5, A9; :: thesis: verum
end;
hence x in a_filter (a_net F) ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in a_filter (a_net F) or x in F \ {{}} )
reconsider xx = x as set by TARSKI:1;
assume A10: x in a_filter (a_net F) ; :: thesis: x in F \ {{}}
then a_net F is_eventually_in xx by Th10;
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 xx ;
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] and
A13: a in f by A1;
A14: the carrier of (BoolePoset ([#] T)) = bool ([#] T) by A2, YELLOW_1:1;
A15: f c= xx
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f or x in xx )
assume A16: x in f ; :: thesis: x in xx
then reconsider b = x as Element of T by A14;
[b,f] in the carrier of (a_net F) by A1, A16;
then reconsider j = [b,f] as Element of (a_net F) ;
A17: j `2 = f ;
j `1 = b ;
then A18: (a_net F) . j = b by Def4;
i `2 = f by A12;
then i <= j by A17, Def4;
hence x in xx by A11, A18; :: thesis: verum
end;
x is Subset of T by A10, Th10;
then A19: x in F by A15, WAYBEL_7:7;
not x in {{}} by A13, A15, TARSKI:def 1;
hence x in F \ {{}} by A19, XBOOLE_0:def 5; :: thesis: verum