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