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