In the book of Euclidean and Non-Euclidean Geometry by Greenberg, it is argued that in a projective plane, the line at infinity forms a closed loop; However the author does not provide any formal justification for this statement, so
Is there any formal proof of this statement from the axioms of projective plane ?
The question comes down to what the author means by a closed loop. I'll give an intuitive explanation. And for this, I'll assume the P(2) space.
Think of the coordinate $\begin{bmatrix}2\\ 3\\ 0\end{bmatrix}$. This coordinate is on the line at infinity in the direction $(2,3)$. In general, the coordinate $\begin{bmatrix}x\\ y\\ 0\end{bmatrix}$ lies on the line at infinity in the direction $(x,y)$. So you see we have a point on the line of infinity in all directions. And thus, the line at infinity forms a closed loop.