ct.category theory - F is ultrafilter over a Boolean algebra implies that for every b, either b or not-b is in F?

Assume you have a proper filter $F$ that avoids both $b$ and $neg b$. Then, you could consider the filter generated by $Fcup{b}$ - which is to say the smallest filter $F'$ containing $F$ and $b$.

Since $F$ was a proper filter it follows that $0notin F$.

If $0in F'$, then this means that there is some $fin F'$ such that $bwedge f = 0$. Now, $neg b=0veeneg b=(bwedge f)veeneg b=(bveeneg b)wedge(fveeneg b)=1wedge(fveeneg b)=fveeneg b$. Thus $f≤neg b$, which means that $neg bin F'$.

Since $neg bin F'$, either $neg bin F$ or $neg b$ may be acquired by meets and upwards closures from $Fcup{b}$. Say $bwedge f≤neg b$ for some $fin F$. Then $bwedge f= bwedge fwedgeneg b = bwedgeneg bwedge f = 0wedge f = 0$ for an $fin F$ and by the above argument, we derive $neg bin F$. This is a contradiction, from which we can derive that $0notin F$.

Hence, $0notin F'$, and thus $F'$ is a proper ideal strictly containing $F$.