let x be bound_QC-variable; :: thesis: for r being Element of CQC-WFF holds r . x = r
let r be Element of CQC-WFF ; :: thesis: r . x = r
Free r = {} by Th13;
hence r . x = r by Th39; :: thesis: verum