set p1 = the non zero Polynomial of L;
set p2 = the non zero Polynomial of L;
take [ the non zero Polynomial of L, the non zero Polynomial of L] ; :: thesis: not [ the non zero Polynomial of L, the non zero Polynomial of L] is zero
thus not [ the non zero Polynomial of L, the non zero Polynomial of L] is zero ; :: thesis: verum