thus L `1 is finite ; :: thesis: verum