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 `)
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: (UFilter BL) . (a `) c= (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;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (UFilter BL) . (a `) or x in (ultraset BL) \ ((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