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