let A be non empty set ; :: thesis: for x, y being bound_QC-variable
for p, q being Element of CQC-WFF
for J being interpretation of A
for s being QC-formula 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; :: thesis: for p, q being Element of CQC-WFF
for J being interpretation of A
for s being QC-formula 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 ; :: thesis: for J being interpretation of A
for s being QC-formula 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 A; :: thesis: for s being QC-formula 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; :: 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

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

A6: now

let u be Element of Valuations_in A; :: thesis: (Valid (q,J)) . u = TRUE
consider w being Element of Valuations_in A such that
A7: ( ( for z being bound_QC-variable 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, Th42;
J,w |= p by A4, Def13;
then A9: (Valid (p,J)) . w = TRUE by Def12;
not x in still_not-bound_in q by A2, A3, A5, Th43;
hence (Valid (q,J)) . u = TRUE by A7, A8, A9, Th39; :: thesis: verum

end;

now

let v be Element of Valuations_in A; :: thesis: J,v |= q
(Valid (q,J)) . v = TRUE by A6;
hence J,v |= q by Def12; :: thesis: verum

end;

hence J |= q by Def13; :: thesis: verum

end;

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