consider q being SubtreeSeq of sy;
q is FinSequence of S -Terms V ;
hence ex b₁ being FinSequence of S -Terms V st b₁ is SubtreeSeq of sy ; :: thesis: verum