take Liouville_constant ; :: thesis: Liouville_constant is liouville
thus Liouville_constant is liouville ; :: thesis: verum