(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