set o = the OperSymbol of S;
set p = the Element of Args ( the OperSymbol of S,(Free (S,X)));
take the OperSymbol of S -term the Element of Args ( the OperSymbol of S,(Free (S,X))) ; :: thesis: the OperSymbol of S -term the Element of Args ( the OperSymbol of S,(Free (S,X))) is compound
thus the OperSymbol of S -term the Element of Args ( the OperSymbol of S,(Free (S,X))) is compound ; :: thesis: verum