consider L being FinSequence such that
A1: Subformulae H = rng L by Th207;
thus Subformulae H is finite by A1; :: thesis: verum