let B be B_Lattice; :: thesis: for a, b being Element of B st a <> b holds
ex FB being Filter of B st
( FB is being_ultrafilter & ( ( a in FB & not b in FB ) or ( not a in FB & b in FB ) ) )
let a, b be Element of B; :: thesis: ( a <> b implies ex FB being Filter of B st
( FB is being_ultrafilter & ( ( a in FB & not b in FB ) or ( not a in FB & b in FB ) ) ) )
assume a <> b ; :: thesis: ex FB being Filter of B st
( FB is being_ultrafilter & ( ( a in FB & not b in FB ) or ( not a in FB & b in FB ) ) )
then ( not a [= b or not b [= a ) by LATTICES:8;
then ( a "/\" (b `) <> Bottom B or b "/\" (a `) <> Bottom B ) by Th43;
then ( ex FB being Filter of B st
( a "/\" (b `) in FB & FB is being_ultrafilter ) or ex FB being Filter of B st
( b "/\" (a `) in FB & FB is being_ultrafilter ) ) by Th20;
then consider FB being Filter of B such that
A1: FB is being_ultrafilter and
A2: ( a "/\" (b `) in FB or b "/\" (a `) in FB ) ;
take FB ; :: thesis: ( FB is being_ultrafilter & ( ( a in FB & not b in FB ) or ( not a in FB & b in FB ) ) )
thus FB is being_ultrafilter by A1; :: thesis: ( ( a in FB & not b in FB ) or ( not a in FB & b in FB ) )
( ( a in FB & b ` in FB ) or ( b in FB & a ` in FB ) ) by A2, Th8;
hence ( ( a in FB & not b in FB ) or ( not a in FB & b in FB ) ) by A1, Th46; :: thesis: verum