set o9 = the s9 -dependent OperSymbol of S9;
set p9 = the x9 -context_including Element of Args ( the s9 -dependent OperSymbol of S9,(Free (S9,X9)));
take t = the s9 -dependent OperSymbol of S9 -term the x9 -context_including Element of Args ( the s9 -dependent OperSymbol of S9,(Free (S9,X9))); :: thesis: ( t is x9 -context & t is compound )
thus t is x9 -context ; :: thesis: t is compound
thus t is compound ; :: thesis: verum