let T be non empty 1-sorted ; for F being Filter of (BoolePoset ([#] T)) holds F \ {{}} = a_filter (a_net F)
let F be Filter of (BoolePoset ([#] T)); 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)
XBOOLE_0:def 10 a_filter (a_net F) c= F \ {{}}
let x be object ; TARSKI:def 3 ( 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)
; 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
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; verum