let Sub be CQC_Substitution; :: thesis: ex S being Element of CQC-Sub-WFF st
( S `1 = VERUM & S `2 = Sub )
reconsider S = [VERUM,Sub] as Element of QC-Sub-WFF by QC_LANG1:def 13, SUBSTUT1:def 16;
take S ; :: thesis: ( S is Element of CQC-Sub-WFF & S `1 = VERUM & S `2 = Sub )
S `1 = VERUM by MCART_1:7;
then S in CQC-Sub-WFF by SUBSTUT1:def 39;
then reconsider S = S as Element of CQC-Sub-WFF ;
S `2 = Sub by MCART_1:7;
hence ( S is Element of CQC-Sub-WFF & S `1 = VERUM & S `2 = Sub ) by MCART_1:7; :: thesis: verum