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