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 ) )

( F = x & F is being_ultrafilter & a in F ) implies x in (UFilter BL) . a )

( F = x & F is being_ultrafilter & a in F ) ) by A1; :: thesis: verum

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

( ex F being Filter of BL st
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;( 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

( F = x & F is being_ultrafilter & a in F ) implies x in (UFilter BL) . a )

proof

hence
( x in (UFilter BL) . a iff ex F being Filter of BL st
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;( 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

( F = x & F is being_ultrafilter & a in F ) ) by A1; :: thesis: verum