let Al be QC-alphabet ; :: thesis: for A being non empty set
for x, y being bound_QC-variable of Al
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A
for s being QC-formula of Al st p = s . x & q = s . y & not x in still_not-bound_in s & J |= p holds
J |= q
let A be non empty set ; :: thesis: for x, y being bound_QC-variable of Al
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A
for s being QC-formula of Al st p = s . x & q = s . y & not x in still_not-bound_in s & J |= p holds
J |= q
let x, y be bound_QC-variable of Al; :: thesis: for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A
for s being QC-formula of Al st p = s . x & q = s . y & not x in still_not-bound_in s & J |= p holds
J |= q
let p, q be Element of CQC-WFF Al; :: thesis: for J being interpretation of Al,A
for s being QC-formula of Al st p = s . x & q = s . y & not x in still_not-bound_in s & J |= p holds
J |= q
let J be interpretation of Al,A; :: thesis: for s being QC-formula of Al st p = s . x & q = s . y & not x in still_not-bound_in s & J |= p holds
J |= q
let s be QC-formula of Al; :: thesis: ( p = s . x & q = s . y & not x in still_not-bound_in s & J |= p implies J |= q )
assume that
A1: p = s . x and
A2: q = s . y and
A3: not x in still_not-bound_in s and
A4: J |= p ; :: thesis: J |= q

now :: thesis: ( x <> y implies J |= q )

assume A5: x <> y ; :: thesis: J |= q

A6: now :: thesis: for u being Element of Valuations_in (Al,A) holds (Valid (q,J)) . u = TRUE

let u be Element of Valuations_in (Al,A); :: thesis: (Valid (q,J)) . u = TRUE
consider w being Element of Valuations_in (Al,A) such that
A7: ( ( for z being bound_QC-variable of Al st z <> x holds
w . z = u . z ) & w . x = u . y ) by Lm3;
w . x = w . y by A7;
then A8: (Valid (p,J)) . w = (Valid (q,J)) . w by A1, A2, Th30;
J,w |= p by A4;
then A9: (Valid (p,J)) . w = TRUE ;
not x in still_not-bound_in q by A2, A3, A5, Th31;
hence (Valid (q,J)) . u = TRUE by A7, A8, A9, Th27; :: thesis: verum

end;

for v being Element of Valuations_in (Al,A) holds J,v |= q by A6;
hence J |= q ; :: thesis: verum

end;

hence J |= q by A1, A2, A4; :: thesis: verum