ex L being FinSequence st Subformulae H = rng L by Th3;
hence Subformulae H is finite ; :: thesis: verum