take 1_. L ; :: thesis: ( not 1_. L is zero & 1_. L is constant )
thus ( not 1_. L is zero & 1_. L is constant ) ; :: thesis: verum