All (B `2 ),((B `1 ) `1 ) in CQC-WFF ;
then (Sub_All B,SQ) `1 in CQC-WFF by A1, Th27;
then Sub_All B,SQ in CQC-Sub-WFF by SUBSTUT1:def 39;
hence Sub_All B,SQ is Element of CQC-Sub-WFF ; :: thesis: verum