take t = x -term ; :: thesis: ( t is x -context & not t is compound )
thus ( t is x -context & not t is compound ) ; :: thesis: verum