let B be B_Lattice; :: thesis: for IB being Ideal of B holds
( ( IB <> (.B.> & IB is prime ) iff IB is_max-ideal )
let IB be Ideal of B; :: thesis: ( ( IB <> (.B.> & IB is prime ) iff IB is_max-ideal )
reconsider F = IB .: as Filter of (B .: ) ;
<.(B .: ).) = (.B.> ;
then ( ( F <> (.B.> & F is prime ) iff F is being_ultrafilter ) by FILTER_0:58;
hence ( ( IB <> (.B.> & IB is prime ) iff IB is_max-ideal ) by Th33, Th44; :: thesis: verum