let B be B_Lattice; :: thesis: for FB being Filter of B st FB is being_ultrafilter holds
for a being Element of B holds
( a in FB iff not a ` in FB )
let FB be Filter of B; :: thesis: ( FB is being_ultrafilter implies for a being Element of B holds
( a in FB iff not a ` in FB ) )
assume A1: FB is being_ultrafilter ; :: thesis: for a being Element of B holds
( a in FB iff not a ` in FB )
let a be Element of B; :: thesis: ( a in FB iff not a ` in FB )
thus ( a in FB implies not a ` in FB ) :: thesis: ( not a ` in FB implies a in FB )

proof

assume ( a in FB & a ` in FB ) ; :: thesis: contradiction
then a "/\" (a `) in FB by Th8;
then Bottom B in FB by LATTICES:20;
then FB = the carrier of B by Th26;
hence contradiction by A1; :: thesis: verum

end;

thus ( not a ` in FB implies a in FB ) by A1, Th44; :: thesis: verum