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