A1: ( (QScope p,x,Sub) `1 = [p,(CFQ . [(All x,p),Sub])] & (QScope p,x,Sub) `2 = x ) by MCART_1:7;
then A2: ( ((QScope p,x,Sub) `1 ) `2 = CFQ . [(All x,p),Sub] & ((QScope p,x,Sub) `1 ) `1 = p ) by MCART_1:7;
((QScope p,x,Sub) `1 ) `2 = (QSub | CQC-Sub-WFF ) . [(All x,p),Sub] by A1, MCART_1:7;
then A3: ((QScope p,x,Sub) `1 ) `2 = QSub . [(All x,p),Sub] by FUNCT_1:72;
then QScope p,x,Sub is quantifiable by A1, A2, SUBSTUT1:def 22;
hence Sub is second_Q_comp of QScope p,x,Sub by A1, A2, A3, SUBSTUT1:def 23; :: thesis: verum