Cholesky Factorisation of a Symmetric Positive Definite Real Matrix

Let $n$ be a natural number with $1\le n$, let $\mathbb{R}$ be the real numbers with the order $\le$ of its ordered field structure, let $[n]$ be the initial segment determined by $n$, and let $G$ be a symmetric positive definite real $n\times n$ matrix. Write $PQ$ for the matrix product and $P^{\top}$ for the transpose. Call a real $n\times n$ matrix $L$ lower triangular if $L_{il}=0$ whenever $i,l\in[n]$ and $i<l$.

Then there exists a lower triangular real $n\times n$ matrix $L$ with $0<L_{ii}$ for every $i\in[n]$ such that

$$G=L\,L^{\top}.$$