let X be Subset of CQC-WFF ; :: thesis: for p being Element of CQC-WFF st still_not-bound_in X is finite holds
still_not-bound_in (X \/ {p}) is finite
let p be Element of CQC-WFF ; :: thesis: ( still_not-bound_in X is finite implies still_not-bound_in (X \/ {p}) is finite )
assume A1: still_not-bound_in X is finite ; :: thesis: still_not-bound_in (X \/ {p}) is finite
still_not-bound_in p is finite by CQC_SIM1:20;
then still_not-bound_in {p} is finite by Th26;
then (still_not-bound_in X) \/ (still_not-bound_in {p}) is finite by A1;
hence still_not-bound_in (X \/ {p}) is finite by Th27; :: thesis: verum