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 Th33;
let a be Element of B; :: thesis: ( a in IB iff not a ` in IB )
(a .: ) ` = a ` by Lm3;
hence ( a in IB iff not a ` in IB ) by A1, FILTER_0:59; :: thesis: verum