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