let B be B_Lattice; :: thesis: for IB being Ideal of B holds
( IB is max-ideal iff ( IB <> the carrier of B & ( for a being Element of B holds
( a in IB or a ` in IB ) ) ) )
let IB be Ideal of B; :: thesis: ( IB is max-ideal iff ( IB <> the carrier of B & ( for a being Element of B holds
( a in IB or a ` in IB ) ) ) )
reconsider FB = IB .: as Filter of (B .:) ;
A1: ( FB is being_ultrafilter iff ( FB <> H₁(B .: ) & ( for a being Element of (B .:) holds
( a in FB or a ` in FB ) ) ) ) by FILTER_0:44;
thus ( IB is max-ideal implies ( IB <> H<sub>1</sub>(B) & ( for a being Element of B holds
( a in IB or a ` in IB ) ) ) ) :: thesis: ( IB <> the carrier of B & ( for a being Element of B holds
( a in IB or a ` in IB ) ) implies IB is max-ideal )

proof

assume A2: IB is max-ideal ; :: thesis: ( IB <> H₁(B) & ( for a being Element of B holds
( a in IB or a ` in IB ) ) )
hence IB <> H<sub>1</sub>(B) ; :: thesis: for a being Element of B holds
( a in IB or a ` in IB )
let a be Element of B; :: thesis: ( a in IB or a ` in IB )
reconsider b = a as Element of (B .:) ;
( b in FB or ( b ` in FB & (a .:) ` = a ` ) ) by A1, A2, Th32, Th54;
hence ( a in IB or a ` in IB ) ; :: thesis: verum

end;

assume that
A3: IB <> H₁(B) and
A4: for a being Element of B holds
( a in IB or a ` in IB ) ; :: thesis: IB is max-ideal

now :: thesis: for a being Element of (B .:) holds
( a in FB or a ` in FB )

let a be Element of (B .:); :: thesis: ( a in FB or a ` in FB )
reconsider b = a as Element of B ;
( b in FB or ( b ` in FB & (.: a) ` = a ` ) ) by A4, Th54;
hence ( a in FB or a ` in FB ) ; :: thesis: verum

end;

hence IB is max-ideal by A1, A3, Th32; :: thesis: verum