take 0._ L ; :: thesis: 0._ L is normalized
thus 0._ L is normalized ; :: thesis: verum