let B be B_Lattice; :: thesis: for FB being Filter of B holds
( FB is being_ultrafilter iff ( FB <> the carrier of B & ( for a being Element of B holds
( a in FB or a ` in FB ) ) ) )
let FB be Filter of B; :: thesis: ( FB is being_ultrafilter iff ( FB <> the carrier of B & ( for a being Element of B holds
( a in FB or a ` in FB ) ) ) )
thus ( FB is being_ultrafilter implies ( FB <> the carrier of B & ( for a being Element of B holds
( a in FB or a ` in FB ) ) ) ) :: thesis: ( FB <> the carrier of B & ( for a being Element of B holds
( a in FB or a ` in FB ) ) implies FB is being_ultrafilter )

proof

reconsider I = B as I_Lattice ;
assume that
A1: FB <> the carrier of B and
A2: for HB being Filter of B st FB c= HB & HB <> the carrier of B holds
FB = HB ; :: according to FILTER_0:def 3 :: thesis: ( FB <> the carrier of B & ( for a being Element of B holds
( a in FB or a ` in FB ) ) )
thus FB <> the carrier of B by A1; :: 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 )
assume A3: not a in FB ; :: thesis: a ` in FB
A4: a in <.a.) ;
A5: FB \/ <.a.) c= <.(FB \/ <.a.)).) by Def4;
<.a.) c= FB \/ <.a.) by XBOOLE_1:7;
then <.a.) c= <.(FB \/ <.a.)).) by A5;
then ( FB c= FB \/ <.a.) & FB <> <.(FB \/ <.a.)).) ) by A3, A4, XBOOLE_1:7;
then <.(FB \/ <.a.)).) = the carrier of B by A2, A5, XBOOLE_1:1;
then A6: a ` in <.(FB \/ <.a.)).) ;
reconsider a9 = a as Element of I ;
reconsider FI = FB as Filter of I ;
A7: a => (a `) = (a `) "\/" (a `) by Th42;
<.{a}.) = <.a.) by Th24;
then A8: a9 ` in <.(FI \/ {a9}).) by A6, Th34;
FB = <.FB.) by Th21;
then a => (a `) in FB by A8, Th40;
hence a ` in FB by A7; :: thesis: verum

end;

assume that
A9: FB <> the carrier of B and
A10: for a being Element of B holds
( a in FB or a ` in FB ) ; :: thesis: FB is being_ultrafilter
thus FB <> the carrier of B by A9; :: according to FILTER_0:def 3 :: thesis: for H being Filter of B st FB c= H & H <> the carrier of B holds
FB = H
let HB be Filter of B; :: thesis: ( FB c= HB & HB <> the carrier of B implies FB = HB )
assume that
A11: FB c= HB and
A12: HB <> the carrier of B and
A13: FB <> HB ; :: thesis: contradiction
not for x being object holds
( x in FB iff x in HB ) by A13, TARSKI:2;
then consider x being set such that
A14: x in HB and
A15: not x in FB by A11;
reconsider x = x as Element of HB by A14;
x ` in FB by A10, A15;
then (x `) "/\" x in HB by A11, Th8;
then A16: Bottom B in HB by LATTICES:20;
HB = <.HB.) by Th21;
hence contradiction by A12, A16, Th25; :: thesis: verum