let B be B_Lattice; :: thesis: for a, b being Element of B st a <> b holds
ex IB being Ideal of B st
( IB is max-ideal & ( ( a in IB & not b in IB ) or ( not a in IB & b in IB ) ) )
let a, b be Element of B; :: thesis: ( a <> b implies ex IB being Ideal of B st
( IB is max-ideal & ( ( a in IB & not b in IB ) or ( not a in IB & b in IB ) ) ) )
assume a <> b ; :: thesis: ex IB being Ideal of B st
( IB is max-ideal & ( ( a in IB & not b in IB ) or ( not a in IB & b in IB ) ) )
then consider FB being Filter of (B .:) such that
A1: FB is being_ultrafilter and
A2: ( ( a .: in FB & not b .: in FB ) or ( not a .: in FB & b .: in FB ) ) by FILTER_0:47;
take IB = .: FB; :: thesis: ( IB is max-ideal & ( ( a in IB & not b in IB ) or ( not a in IB & b in IB ) ) )
IB .: = FB ;
hence IB is max-ideal by A1, Th32; :: thesis: ( ( a in IB & not b in IB ) or ( not a in IB & b in IB ) )
thus ( ( a in IB & not b in IB ) or ( not a in IB & b in IB ) ) by A2; :: thesis: verum