Formal proof that $ax+by+c \le 0$ defines a halfplane 
The condition $ax+by+c \le 0$ defines a halfplane

How do I formally prove that? My reasoning is this:
Chosen $(x_1, y_1)$ such that $ax_1+by_1+c=0$, the inequality $y\le-(ax_1/b+c/b)$ is true for any $y$ such that $y\le y_1$. These points will lie “on the same side” of the plane in respect to the line (is it even allowed to say something like this in a formal, complete proof? How should I say it?)
Thank you in advance
 A: Suppose $ax+by+c=0$ represents a line (that is, not both $a$ and $b$ are $0$).
I maintain that the plane is divided into three subsets:
\begin{align}
H_0&=\{(x,y):ax+by+c=0\}\\[4px]
H_+&=\{(x,y):ax+by+c>0\}\\[4px]
H_-&=\{(x,y):ax+by+c<0\}
\end{align}
with the properties


*

*If $A,B\in H_+$, then the segment joining $A$ and $B$ is contained in $H_+$

*If $A,B\in H_-$, then the segment joining $A$ and $B$ is contained in $H_-$

*If $A\in H_+$ and $B\in H_-$, then the segment joining $A$ and $B$ intersects $H_0$


If $A=(x_1,y_1)$ and $B=(x_2,y_2)$, then the segment joining $A$ and $B$ consists of the points of the form $((1-t)x_1+tx_2,(1-t)y_1+ty_2)$, for $t\in[0,1]$.
Consider $f_{AB}\colon [0,1]\to\mathbb{R}$ defined by
$$
f_{AB}(t)=a((1-t)x_1+tx_2)+b((1-t)y_1+ty_2)+c
$$
where $A$ and $B$ are any two distinct points. Then $f_{AB}$ is clearly continuous and vanishes at most at one point because it is either increasing or decreasing (being the restriction of a degree $1$ polynomial).
Suppose $A,B\in H_+$ and that the segment contains a point $C\notin H_+$, corresponding to $t_0\in(0,1)$. Then either $C\in H_0$ or $C\in H_-$. Since $f_{AB}(0)>0$, we deduce that $f$ is decreasing, so $f(1)<0$ and $B\in H_-$: a contradiction. This proves 1.
Statement 2 is similar.
For 3, we have $f_{AB}(0)>0$ and $f_{AB}(1)<0$, so there is $t\in(0,1)$ such that $f_{AB}(t_0)=0$. This corresponds to a point on the segment belonging to $H_0$.
It follows that the segment connecting any two points in $H_0\cup H_-$ is entirely contained in $H_0\cup H_-$, which corresponds to the geometric notion of halfplane. I leave to you proving that $H_0$ is indeed the boundary (in the topological sense) of $H_0\cup H_-$.
