let Al be QC-alphabet ; 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 ; 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; 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; 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; 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; ( 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
; J |= q
now ( x <> y implies J |= q )assume A5:
x <> y
;
J |= qA6:
now for u being Element of Valuations_in (Al,A) holds (Valid (q,J)) . u = TRUE let u be
Element of
Valuations_in (
Al,
A);
(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;
verum end;
for
v being
Element of
Valuations_in (
Al,
A) holds
J,
v |= q
by A6;
hence
J |= q
;
verum end;
hence
J |= q
by A1, A2, A4; verum