let Al be QC-alphabet ; :: thesis: for p, q 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 ) ) & ( for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = q & S `2 = Sub ) ) holds

for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = p '&' q & S `2 = Sub )

let p, q 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 ) ) & ( for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = q & S `2 = Sub ) ) implies for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = p '&' q & S `2 = Sub ) )

assume that

A1: for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = p & S `2 = Sub ) and

A2: for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = q & S `2 = Sub ) ; :: thesis: for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = p '&' q & S `2 = Sub )

let Sub be CQC_Substitution of Al; :: thesis: ex S being Element of CQC-Sub-WFF Al st

( S `1 = p '&' q & S `2 = Sub )

consider S1 being Element of CQC-Sub-WFF Al such that

A3: ( S1 `1 = p & S1 `2 = Sub ) by A1;

consider S2 being Element of CQC-Sub-WFF Al such that

A4: ( S2 `1 = q & S2 `2 = Sub ) by A2;

S2 = [q,Sub] by A4, SUBSTUT1:10;

then [q,Sub] in QC-Sub-WFF Al ;

then A5: [(@ q),Sub] in QC-Sub-WFF Al by QC_LANG1:def 13;

S1 = [p,Sub] by A3, SUBSTUT1:10;

then [p,Sub] in QC-Sub-WFF Al ;

then [(@ p),Sub] in QC-Sub-WFF Al by QC_LANG1:def 13;

then [((<*[2,0]*> ^ (@ p)) ^ (@ q)),Sub] in QC-Sub-WFF Al by A5, SUBSTUT1:def 16;

then reconsider S = [(p '&' q),Sub] as Element of QC-Sub-WFF Al by QC_LANG1:def 16;

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 A6: 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 = p '&' q & S `2 = Sub )

S `1 = p '&' q ;

then reconsider S = S as Element of CQC-Sub-WFF Al by A6;

S `2 = Sub ;

hence ( S is Element of CQC-Sub-WFF Al & S `1 = p '&' q & S `2 = Sub ) ; :: thesis: verum

( S `1 = p & S `2 = Sub ) ) & ( for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = q & S `2 = Sub ) ) holds

for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = p '&' q & S `2 = Sub )

let p, q 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 ) ) & ( for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = q & S `2 = Sub ) ) implies for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = p '&' q & S `2 = Sub ) )

assume that

A1: for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = p & S `2 = Sub ) and

A2: for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = q & S `2 = Sub ) ; :: thesis: for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = p '&' q & S `2 = Sub )

let Sub be CQC_Substitution of Al; :: thesis: ex S being Element of CQC-Sub-WFF Al st

( S `1 = p '&' q & S `2 = Sub )

consider S1 being Element of CQC-Sub-WFF Al such that

A3: ( S1 `1 = p & S1 `2 = Sub ) by A1;

consider S2 being Element of CQC-Sub-WFF Al such that

A4: ( S2 `1 = q & S2 `2 = Sub ) by A2;

S2 = [q,Sub] by A4, SUBSTUT1:10;

then [q,Sub] in QC-Sub-WFF Al ;

then A5: [(@ q),Sub] in QC-Sub-WFF Al by QC_LANG1:def 13;

S1 = [p,Sub] by A3, SUBSTUT1:10;

then [p,Sub] in QC-Sub-WFF Al ;

then [(@ p),Sub] in QC-Sub-WFF Al by QC_LANG1:def 13;

then [((<*[2,0]*> ^ (@ p)) ^ (@ q)),Sub] in QC-Sub-WFF Al by A5, SUBSTUT1:def 16;

then reconsider S = [(p '&' q),Sub] as Element of QC-Sub-WFF Al by QC_LANG1:def 16;

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 A6: 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 = p '&' q & S `2 = Sub )

S `1 = p '&' q ;

then reconsider S = S as Element of CQC-Sub-WFF Al by A6;

S `2 = Sub ;

hence ( S is Element of CQC-Sub-WFF Al & S `1 = p '&' q & S `2 = Sub ) ; :: thesis: verum