let B be B_Lattice; :: thesis: for FB being Filter of B holds
( ( FB <> <.B.) & FB is prime ) iff FB is being_ultrafilter )
let FB be Filter of B; :: thesis: ( ( FB <> <.B.) & FB is prime ) iff FB is being_ultrafilter )
thus ( FB <> <.B.) & FB is prime implies FB is being_ultrafilter ) :: thesis: ( FB is being_ultrafilter implies ( FB <> <.B.) & FB is prime ) )

proof

assume that
A1: FB <> <.B.) and
A2: for a, b being Element of B holds
( a "\/" b in FB iff ( a in FB or b in FB ) ) ; :: according to FILTER_0:def 5 :: thesis: FB is being_ultrafilter

now :: thesis: for a being Element of B st not a in FB holds
a ` in FB

let a be Element of B; :: thesis: ( not a in FB implies a ` in FB )
assume A3: not a in FB ; :: thesis: a ` in FB
a "\/" (a `) = Top B by LATTICES:21;
then a "\/" (a `) in FB by Th11;
hence a ` in FB by A2, A3; :: thesis: verum

end;

hence FB is being_ultrafilter by A1, Th44; :: thesis: verum

end;

assume A4: FB is being_ultrafilter ; :: thesis: ( FB <> <.B.) & FB is prime )
hence FB <> <.B.) ; :: thesis: FB is prime
let a be Element of B; :: according to FILTER_0:def 5 :: thesis: for q being Element of B holds
( a "\/" q in FB iff ( a in FB or q in FB ) )
let b be Element of B; :: thesis: ( a "\/" b in FB iff ( a in FB or b in FB ) )
A5: FB <> the carrier of B by A4;
thus ( not a "\/" b in FB or a in FB or b in FB ) :: thesis: ( ( a in FB or b in FB ) implies a "\/" b in FB )

proof

assume that
A6: a "\/" b in FB and
A7: ( not a in FB & not b in FB ) ; :: thesis: contradiction
( a ` in FB & b ` in FB ) by A4, A7, Th44;
then (a `) "/\" (b `) in FB by Th8;
then (a "\/" b) ` in FB by LATTICES:24;
then (a "\/" b) "/\" ((a "\/" b) `) in FB by A6, Th8;
then A8: Bottom B in FB by LATTICES:20;
FB = <.FB.) by Th21;
hence contradiction by A5, A8, Th25; :: thesis: verum

end;

thus ( ( a in FB or b in FB ) implies a "\/" b in FB ) by Th10; :: thesis: verum