printf ("@def@item{@filbreak@vskip5pt@ITEM}\n");
printf ("@font@tensy cmsy10 scaled @magstephalf\n");
printf ("@font@teni cmmi10 scaled @magstephalf\n");
printf ("@def@item{@filbreak@vskip5pt@ITEM}\n");
printf ("@font@tensy cmsy10 scaled @magstephalf\n");
printf ("@font@teni cmmi10 scaled @magstephalf\n");