let A be QC-alphabet ; :: thesis: for x being bound_QC-variable of A
for r being Element of CQC-WFF A holds r . x = r
let x be bound_QC-variable of A; :: thesis: for r being Element of CQC-WFF A holds r . x = r
let r be Element of CQC-WFF A; :: thesis: r . x = r
Free r = {} by Th4;
hence r . x = r by Th26; :: thesis: verum