take s = {(0_. L)}; :: thesis: ( not s is empty & s is L -polynomial-membered )
thus not s is empty ; :: thesis: s is L -polynomial-membered
thus s is L -polynomial-membered by TARSKI:def 1; :: thesis: verum