A1: { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables ) } = {} by Th15;
{ (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables ) } = {} by Th15;
hence P ! l is Element of CQC-WFF by A1, Th17; :: thesis: verum