let B be B_Lattice; :: thesis: for IB being Ideal of B st IB is max-ideal holds
for a being Element of B holds
( a in IB iff not a ` in IB )
let IB be Ideal of B; :: thesis: ( IB is max-ideal implies for a being Element of B holds
( a in IB iff not a ` in IB ) )
reconsider FB = IB .: as Filter of (B .:) ;
assume IB is max-ideal ; :: thesis: for a being Element of B holds
( a in IB iff not a ` in IB )
then A1: FB is being_ultrafilter by Th32;
let a be Element of B; :: thesis: ( a in IB iff not a ` in IB )
(a .:) ` = a ` by Lm4;
hence ( a in IB iff not a ` in IB ) by A1, FILTER_0:46; :: thesis: verum