let S be Element of QC-Sub-WFF ; :: thesis: ex p being QC-formula ex e being Element of vSUB st S = [p,e]
[:QC-WFF,vSUB:] is QC-Sub-closed by Def16, Th7;
then QC-Sub-WFF c= [:QC-WFF,vSUB:] by Def17;
then S in [:QC-WFF,vSUB:] by TARSKI:def 3;
then consider a, b being set such that
A1: a in QC-WFF and
A2: b in vSUB and
A3: S = [a,b] by ZFMISC_1:def 2;
reconsider e = b as Element of vSUB by A2;
reconsider p = a as Element of QC-WFF by A1;
take p ; :: thesis: ex e being Element of vSUB st S = [p,e]
take e ; :: thesis: S = [p,e]
thus S = [p,e] by A3; :: thesis: verum