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 & q = s . y ) and
A2: not x in still_not-bound_in s and
A3: J |= p ; :: thesis: J |= q

now

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

A5: 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
A6: ( ( for z being bound_QC-variable st z <> x holds
w . z = u . z ) & w . x = u . y ) from VALUAT_1:sch 1();
w . x = w . y by A6;
then A7: (Valid p,J) . w = (Valid q,J) . w by A1, Th42;
J,w |= p by A3, Def13;
then A8: (Valid p,J) . w = TRUE by Def12;
not x in still_not-bound_in q by A1, A2, A4, Th43;
hence (Valid q,J) . u = TRUE by A6, A7, A8, Th39; :: thesis: verum

end;

now

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

end;

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

end;

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