let x be set ; :: thesis: for BL being non trivial B_Lattice
for a being Element of BL holds
( x in (UFilter BL) . a iff ex F being Filter of BL st
( F = x & F is being_ultrafilter & a in F ) )
let BL be non trivial B_Lattice; :: thesis: for a being Element of BL holds
( x in (UFilter BL) . a iff ex F being Filter of BL st
( F = x & F is being_ultrafilter & a in F ) )
let a be Element of BL; :: thesis: ( x in (UFilter BL) . a iff ex F being Filter of BL st
( F = x & F is being_ultrafilter & a in F ) )
A1: ( x in (UFilter BL) . a implies ex F being Filter of BL st
( F = x & F is being_ultrafilter & a in F ) )

proof

assume x in (UFilter BL) . a ; :: thesis: ex F being Filter of BL st
( F = x & F is being_ultrafilter & a in F )
then x in { UF where UF is Filter of BL : ( UF is being_ultrafilter & a in UF ) } by Def6;
then consider F being Filter of BL such that
A2: F = x and
A3: F is being_ultrafilter and
A4: a in F ;
take F ; :: thesis: ( F = x & F is being_ultrafilter & a in F )
thus ( F = x & F is being_ultrafilter & a in F ) by A2, A3, A4; :: thesis: verum

end;

( ex F being Filter of BL st
( F = x & F is being_ultrafilter & a in F ) implies x in (UFilter BL) . a )

proof

assume ex F being Filter of BL st
( F = x & F is being_ultrafilter & a in F ) ; :: thesis: x in (UFilter BL) . a
then x in { UF where UF is Filter of BL : ( UF is being_ultrafilter & a in UF ) } ;
hence x in (UFilter BL) . a by Def6; :: thesis: verum

end;

hence ( x in (UFilter BL) . a iff ex F being Filter of BL st
( F = x & F is being_ultrafilter & a in F ) ) by A1; :: thesis: verum