set X = { G where G is Element of QC-Sub-WFF Al : G `1 is Element of CQC-WFF Al } ;
{ G where G is Element of QC-Sub-WFF Al : G `1 is Element of CQC-WFF Al } = CQC-Sub-WFF Al by SUBSTUT1:def 39;
then A1: for G being Element of QC-Sub-WFF Al st G `1 is Element of CQC-WFF Al holds
G in CQC-Sub-WFF Al ;
Sub_P (P,ll,Sub) = [(P ! ll),Sub] by SUBSTUT1:9;
then ( (Sub_P (P,ll,Sub)) `1 = P ! ll & P ! ll in CQC-WFF Al ) ;
hence Sub_P (P,ll,Sub) is Element of CQC-Sub-WFF Al by A1; :: thesis: verum