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:45;
hence ( ( IB <> (.B.> & IB is prime ) iff IB is max-ideal ) by Th32, Th43; :: thesis: verum