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}