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 \ {{}}

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

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

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 a_filter (a_net F) or x in F \ {{}} )
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

end;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

hence
x in a_filter (a_net F)
; :: thesis: verum
take
i
; :: according to WAYBEL_0:def 11 :: thesis: for b_{1} being Element of the carrier of (a_net F) holds

( not i <= b_{1} or (a_net F) . b_{1} 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;( not i <= b

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

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

x is Subset of T
by A10, Th10;
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;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

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