:: deftheorem defines LiouvilleNumbers LIOUVIL1:def 11 :
LiouvilleNumbers = { nl where nl is Liouville : verum } ;