set x = the Element of Vars ;
take the Element of Vars -term C ; :: thesis: not the Element of Vars -term C is compound
thus not the Element of Vars -term C is compound ; :: thesis: verum