div.example {
	display: block;
	margin-top: 5pt;
	margin-bottom: 5pt;
	font-size: 9pt;
}

div.note {
	display: block;
	margin-top: 5pt;
	margin-bottom: 5pt;
	font-size: 9pt;
}

div.note .texttt { font-size: 9pt; }
div.example .texttt { font-size: 9pt; }

div.note .textsf { font-family: 'Noto Sans'; font-size: 9pt; }
div.example .textsf { font-family: 'Noto Sans'; font-size: 9pt; }

div.note .math { font-size: 9pt; }
div.example .math { font-size: 9pt; }