(B `1 ) `2 = QSub . [(All (B `2 ),((B `1 ) `1 )),SQ] by A1, Def23;
then B `1 = [((B `1 ) `1 ),(QSub . [(All (B `2 ),((B `1 ) `1 )),SQ])] by Th10;
hence [(All (B `2 ),((B `1 ) `1 )),SQ] is Element of QC-Sub-WFF by Def16; :: thesis: verum