take 1-sorted(# the non empty L -polynomial-membered set #) ; :: thesis: ( not 1-sorted(# the non empty L -polynomial-membered set #) is empty & 1-sorted(# the non empty L -polynomial-membered set #) is L -polynomial-membered )
thus ( not 1-sorted(# the non empty L -polynomial-membered set #) is empty & 1-sorted(# the non empty L -polynomial-membered set #) is L -polynomial-membered ) ; :: thesis: verum