take the non zero Element of L | L ; :: thesis: ( not the non zero Element of L | L is zero & the non zero Element of L | L is constant )
thus ( not the non zero Element of L | L is zero & the non zero Element of L | L is constant ) ; :: thesis: verum