Let $\exp$ be the D1932: Standard natural real exponential function.
Let $G \in \text{Gaussian}(\mu, \sigma)$ be a D210: Gaussian random real number.
A D3161: Random real number $X \in \text{Random}(\mathbb{R})$ is a log-gaussian random basic real number with parameters $\mu$ and $\sigma$ if and only if
\begin{equation}
X
\overset{d}{=}
\exp( G )
\end{equation}