Sub_P P,ll,Sub = [(P ! ll),Sub] by SUBSTUT1:9;
then (Sub_P P,ll,Sub) `1 = P ! ll by MCART_1:7;
then consider S being Element of QC-Sub-WFF such that
A1: ( S = Sub_P P,ll,Sub & S `1 in CQC-WFF ) ;
Sub_P P,ll,Sub in CQC-Sub-WFF by A1, SUBSTUT1:def 39;
hence Sub_P P,ll,Sub is Element of CQC-Sub-WFF ; :: thesis: verum