let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al st ( for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st
( S `1 = p & S `2 = Sub ) ) holds
for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st
( S `1 = 'not' p & S `2 = Sub )
let p be Element of CQC-WFF Al; :: thesis: ( ( for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st
( S `1 = p & S `2 = Sub ) ) implies for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st
( S `1 = 'not' p & S `2 = Sub ) )
assume A1: for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st
( S `1 = p & S `2 = Sub ) ; :: thesis: for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st
( S `1 = 'not' p & S `2 = Sub )
let Sub be CQC_Substitution of Al; :: thesis: ex S being Element of CQC-Sub-WFF Al st
( S `1 = 'not' p & S `2 = Sub )
consider S being Element of CQC-Sub-WFF Al such that
A2: ( S `1 = p & S `2 = Sub ) by A1;
S = [p,Sub] by A2, SUBSTUT1:10;
then [p,Sub] in QC-Sub-WFF Al ;
then [(@ p),Sub] in QC-Sub-WFF Al by QC_LANG1:def 13;
then [(<*[1,0]*> ^ (@ p)),Sub] in QC-Sub-WFF Al by SUBSTUT1:def 16;
then reconsider S = [('not' p),Sub] as Element of QC-Sub-WFF Al by QC_LANG1:def 15;
set X = { G where G is Element of QC-Sub-WFF Al : G `1 is Element of CQC-WFF Al } ;
{ G where G is Element of QC-Sub-WFF Al : G `1 is Element of CQC-WFF Al } = CQC-Sub-WFF Al by SUBSTUT1:def 39;
then A3: for G being Element of QC-Sub-WFF Al st G `1 is Element of CQC-WFF Al holds
G in CQC-Sub-WFF Al ;
take S ; :: thesis: ( S is Element of CQC-Sub-WFF Al & S `1 = 'not' p & S `2 = Sub )
S `1 = 'not' p ;
then reconsider S = S as Element of CQC-Sub-WFF Al by A3;
S `2 = Sub ;
hence ( S is Element of CQC-Sub-WFF Al & S `1 = 'not' p & S `2 = Sub ) ; :: thesis: verum