reconsider RF = [ the Polynomial of L, the non zero Polynomial of L] as set by TARSKI:1;
take RF ; :: thesis: ex p1 being Polynomial of L ex p2 being non zero Polynomial of L st RF = [p1,p2]
thus ex p1 being Polynomial of L ex p2 being non zero Polynomial of L st RF = [p1,p2] ; :: thesis: verum