let BL be non trivial B_Lattice; :: thesis: for a being Element of BL holds (ultraset BL) \ ((UFilter BL) . a) = (UFilter BL) . (a `)

let a be Element of BL; :: thesis: (ultraset BL) \ ((UFilter BL) . a) = (UFilter BL) . (a `)

assume x in (UFilter BL) . (a `) ; :: thesis: x in (ultraset BL) \ ((UFilter BL) . a)

then consider F being Filter of BL such that

A6: F = x and

A7: F is being_ultrafilter and

A8: a ` in F by Th17;

A9: not a in F by A7, A8, FILTER_0:46;

A10: F in ultraset BL by A7;

not F in (UFilter BL) . a by A9, Th18;

hence x in (ultraset BL) \ ((UFilter BL) . a) by A6, A10, XBOOLE_0:def 5; :: thesis: verum

let a be Element of BL; :: thesis: (ultraset BL) \ ((UFilter BL) . a) = (UFilter BL) . (a `)

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: (UFilter BL) . (a `) c= (ultraset BL) \ ((UFilter BL) . a)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (UFilter BL) . (a `) or x in (ultraset BL) \ ((UFilter BL) . a) )let x be object ; :: thesis: ( x in (ultraset BL) \ ((UFilter BL) . a) implies x in (UFilter BL) . (a `) )

assume A1: x in (ultraset BL) \ ((UFilter BL) . a) ; :: thesis: x in (UFilter BL) . (a `)

then A2: x in ultraset BL by XBOOLE_0:def 5;

A3: not x in (UFilter BL) . a by A1, XBOOLE_0:def 5;

consider F being Filter of BL such that

A4: F = x and

A5: F is being_ultrafilter by A2;

not a in F by A3, A4, A5, Th18;

then a ` in F by A5, FILTER_0:46;

hence x in (UFilter BL) . (a `) by A4, A5, Th18; :: thesis: verum

end;assume A1: x in (ultraset BL) \ ((UFilter BL) . a) ; :: thesis: x in (UFilter BL) . (a `)

then A2: x in ultraset BL by XBOOLE_0:def 5;

A3: not x in (UFilter BL) . a by A1, XBOOLE_0:def 5;

consider F being Filter of BL such that

A4: F = x and

A5: F is being_ultrafilter by A2;

not a in F by A3, A4, A5, Th18;

then a ` in F by A5, FILTER_0:46;

hence x in (UFilter BL) . (a `) by A4, A5, Th18; :: thesis: verum

assume x in (UFilter BL) . (a `) ; :: thesis: x in (ultraset BL) \ ((UFilter BL) . a)

then consider F being Filter of BL such that

A6: F = x and

A7: F is being_ultrafilter and

A8: a ` in F by Th17;

A9: not a in F by A7, A8, FILTER_0:46;

A10: F in ultraset BL by A7;

not F in (UFilter BL) . a by A9, Th18;

hence x in (ultraset BL) \ ((UFilter BL) . a) by A6, A10, XBOOLE_0:def 5; :: thesis: verum