let Al be QC-alphabet ; :: thesis: for X being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al st still_not-bound_in X is finite holds
still_not-bound_in (X \/ {p}) is finite
let X be Subset of (CQC-WFF Al); :: thesis: for p being Element of CQC-WFF Al st still_not-bound_in X is finite holds
still_not-bound_in (X \/ {p}) is finite
let p be Element of CQC-WFF Al; :: 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:19;
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