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 Sub_P (P,ll,Sub) in CQC-Sub-WFF by SUBSTUT1:def 39;
hence Sub_P (P,ll,Sub) is Element of CQC-Sub-WFF ; :: thesis: verum