let Al be QC-alphabet ; :: thesis: for A being non empty set
for x being bound_QC-variable of Al
for p being Element of CQC-WFF Al
for J being interpretation of Al,A st not x in still_not-bound_in p holds
for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid (p,J)) . v = (Valid (p,J)) . w
let A be non empty set ; :: thesis: for x being bound_QC-variable of Al
for p being Element of CQC-WFF Al
for J being interpretation of Al,A st not x in still_not-bound_in p holds
for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid (p,J)) . v = (Valid (p,J)) . w
let x be bound_QC-variable of Al; :: thesis: for p being Element of CQC-WFF Al
for J being interpretation of Al,A st not x in still_not-bound_in p holds
for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid (p,J)) . v = (Valid (p,J)) . w
let p be Element of CQC-WFF Al; :: thesis: for J being interpretation of Al,A st not x in still_not-bound_in p holds
for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid (p,J)) . v = (Valid (p,J)) . w
let J be interpretation of Al,A; :: thesis: ( not x in still_not-bound_in p implies for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid (p,J)) . v = (Valid (p,J)) . w )
defpred S₁[ Element of CQC-WFF Al] means ( not x in still_not-bound_in $1 implies for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid ($1,J)) . v = (Valid ($1,J)) . w );

A1: now :: thesis: for s, t being Element of CQC-WFF Al
for y being bound_QC-variable of Al
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( S₁[ VERUM Al] & S₁[P ! ll] & ( S₁[s] implies S₁[ 'not' s] ) & ( S₁[s] & S₁[t] implies S₁[s '&' t] ) & ( S₁[s] implies S₁[ All (y,s)] ) )

let s, t be Element of CQC-WFF Al; :: thesis: for y being bound_QC-variable of Al
for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( S₁[ VERUM Al] & S₁[P ! ll] & ( S₁[s] implies S₁[ 'not' s] ) & ( S₁[s] & S₁[t] implies S₁[s '&' t] ) & ( S₁[s] implies S₁[ All (y,s)] ) )
let y be bound_QC-variable of Al; :: thesis: for k being Nat
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( S₁[ VERUM Al] & S₁[P ! ll] & ( S₁[s] implies S₁[ 'not' s] ) & ( S₁[s] & S₁[t] implies S₁[s '&' t] ) & ( S₁[s] implies S₁[ All (y,s)] ) )
let k be Nat; :: thesis: for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( S₁[ VERUM Al] & S₁[P ! ll] & ( S₁[s] implies S₁[ 'not' s] ) & ( S₁[s] & S₁[t] implies S₁[s '&' t] ) & ( S₁[s] implies S₁[ All (y,s)] ) )
let ll be CQC-variable_list of k,Al; :: thesis: for P being QC-pred_symbol of k,Al holds
( S₁[ VERUM Al] & S₁[P ! ll] & ( S₁[s] implies S₁[ 'not' s] ) & ( S₁[s] & S₁[t] implies S₁[s '&' t] ) & ( S₁[s] implies S₁[ All (y,s)] ) )
let P be QC-pred_symbol of k,Al; :: thesis: ( S₁[ VERUM Al] & S₁[P ! ll] & ( S₁[s] implies S₁[ 'not' s] ) & ( S₁[s] & S₁[t] implies S₁[s '&' t] ) & ( S₁[s] implies S₁[ All (y,s)] ) )
thus S₁[ VERUM Al] :: thesis: ( S₁[P ! ll] & ( S₁[s] implies S₁[ 'not' s] ) & ( S₁[s] & S₁[t] implies S₁[s '&' t] ) & ( S₁[s] implies S₁[ All (y,s)] ) )

proof

assume not x in still_not-bound_in (VERUM Al) ; :: thesis: for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid ((VERUM Al),J)) . v = (Valid ((VERUM Al),J)) . w
thus for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid ((VERUM Al),J)) . v = (Valid ((VERUM Al),J)) . w :: thesis: verum

proof

let v, w be Element of Valuations_in (Al,A); :: thesis: ( ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) implies (Valid ((VERUM Al),J)) . v = (Valid ((VERUM Al),J)) . w )
assume for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ; :: thesis: (Valid ((VERUM Al),J)) . v = (Valid ((VERUM Al),J)) . w
(Valid ((VERUM Al),J)) . v = TRUE by Th5;
hence (Valid ((VERUM Al),J)) . v = (Valid ((VERUM Al),J)) . w by Th5; :: thesis: verum

end;

end;

A2: rng ll c= bound_QC-variables Al by RELAT_1:def 19;
thus S₁[P ! ll] :: thesis: ( ( S₁[s] implies S₁[ 'not' s] ) & ( S₁[s] & S₁[t] implies S₁[s '&' t] ) & ( S₁[s] implies S₁[ All (y,s)] ) )

proof

assume A3: not x in still_not-bound_in (P ! ll) ; :: thesis: for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid ((P ! ll),J)) . v = (Valid ((P ! ll),J)) . w
thus for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid ((P ! ll),J)) . v = (Valid ((P ! ll),J)) . w :: thesis: verum

proof

let v, w be Element of Valuations_in (Al,A); :: thesis: ( ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) implies (Valid ((P ! ll),J)) . v = (Valid ((P ! ll),J)) . w )
assume A4: for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ; :: thesis: (Valid ((P ! ll),J)) . v = (Valid ((P ! ll),J)) . w

A5: now :: thesis: ( (Valid ((P ! ll),J)) . v = TRUE implies (Valid ((P ! ll),J)) . v = (Valid ((P ! ll),J)) . w )

A6: len (v *' ll) = k by Def3;

A7: now :: thesis: for i being Nat st 1 <= i & i <= len (v *' ll) holds
(v *' ll) . i = (w *' ll) . i

let i be Nat; :: thesis: ( 1 <= i & i <= len (v *' ll) implies (v *' ll) . i = (w *' ll) . i )
assume A8: ( 1 <= i & i <= len (v *' ll) ) ; :: thesis: (v *' ll) . i = (w *' ll) . i
A9: len (v *' ll) = len ll by A6, CARD_1:def 7;
then i in dom ll by A8, FINSEQ_3:25;
then ll . i in rng ll by FUNCT_1:def 3;
then reconsider z = ll . i as bound_QC-variable of Al by A2;
ll . i <> x

proof

reconsider M = still_not-bound_in ll as set ;
not x in M by A3, QC_LANG3:5;
then not x in variables_in (ll,(bound_QC-variables Al)) by QC_LANG3:2;
then not x in { (ll . i2) where i2 is Nat : ( 1 <= i2 & i2 <= len ll & ll . i2 in bound_QC-variables Al ) } by QC_LANG3:def 1;
hence ll . i <> x by A8, A9; :: thesis: verum

end;

then A10: w . z = v . z by A4;
(v *' ll) . i = v . (ll . i) by A6, A8, Def3;
hence (v *' ll) . i = (w *' ll) . i by A6, A8, A10, Def3; :: thesis: verum

end;

assume A11: (Valid ((P ! ll),J)) . v = TRUE ; :: thesis: (Valid ((P ! ll),J)) . v = (Valid ((P ! ll),J)) . w
then (ll 'in' (J . P)) . v = TRUE by Lm1;
then A12: v *' ll in J . P by Def4;
len (w *' ll) = k by Def3;
then w *' ll in J . P by A12, A6, A7, FINSEQ_1:14;
then (ll 'in' (J . P)) . w = TRUE by Def4;
hence (Valid ((P ! ll),J)) . v = (Valid ((P ! ll),J)) . w by A11, Lm1; :: thesis: verum

end;

now :: thesis: ( (Valid ((P ! ll),J)) . v = FALSE implies (Valid ((P ! ll),J)) . v = (Valid ((P ! ll),J)) . w )

A13: len (v *' ll) = k by Def3;

A14: now :: thesis: for i being Nat st 1 <= i & i <= len (v *' ll) holds
(v *' ll) . i = (w *' ll) . i

let i be Nat; :: thesis: ( 1 <= i & i <= len (v *' ll) implies (v *' ll) . i = (w *' ll) . i )
assume A15: ( 1 <= i & i <= len (v *' ll) ) ; :: thesis: (v *' ll) . i = (w *' ll) . i
A16: len (v *' ll) = len ll by A13, CARD_1:def 7;
then i in dom ll by A15, FINSEQ_3:25;
then ll . i in rng ll by FUNCT_1:def 3;
then reconsider z = ll . i as bound_QC-variable of Al by A2;
ll . i <> x

proof

reconsider M = still_not-bound_in ll as set ;
not x in M by A3, QC_LANG3:5;
then not x in variables_in (ll,(bound_QC-variables Al)) by QC_LANG3:2;
then ( i in NAT & not x in { (ll . i2) where i2 is Nat : ( 1 <= i2 & i2 <= len ll & ll . i2 in bound_QC-variables Al ) } ) by ORDINAL1:def 12, QC_LANG3:def 1;
hence ll . i <> x by A15, A16; :: thesis: verum

end;

then A17: w . z = v . z by A4;
(v *' ll) . i = v . (ll . i) by A13, A15, Def3;
hence (v *' ll) . i = (w *' ll) . i by A13, A15, A17, Def3; :: thesis: verum

end;

assume A18: (Valid ((P ! ll),J)) . v = FALSE ; :: thesis: (Valid ((P ! ll),J)) . v = (Valid ((P ! ll),J)) . w
then (ll 'in' (J . P)) . v = FALSE by Lm1;
then A19: not v *' ll in J . P by Def4;
len (w *' ll) = k by Def3;
then not w *' ll in J . P by A19, A13, A14, FINSEQ_1:14;
then (ll 'in' (J . P)) . w = FALSE by Def4;
hence (Valid ((P ! ll),J)) . v = (Valid ((P ! ll),J)) . w by A18, Lm1; :: thesis: verum

end;

hence (Valid ((P ! ll),J)) . v = (Valid ((P ! ll),J)) . w by A5, XBOOLEAN:def 3; :: thesis: verum

end;

end;

thus ( S₁[s] implies S₁[ 'not' s] ) :: thesis: ( ( S₁[s] & S₁[t] implies S₁[s '&' t] ) & ( S₁[s] implies S₁[ All (y,s)] ) )

proof

assume A20: ( ( not x in still_not-bound_in s implies for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid (s,J)) . v = (Valid (s,J)) . w ) & not x in still_not-bound_in ('not' s) ) ; :: thesis: for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w
thus for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w :: thesis: verum

proof

let v, w be Element of Valuations_in (Al,A); :: thesis: ( ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) implies (Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w )
assume A21: for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ; :: thesis: (Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w

A22: now :: thesis: ( (Valid (('not' s),J)) . v = FALSE implies (Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w )

assume A23: (Valid (('not' s),J)) . v = FALSE ; :: thesis: (Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w
then 'not' ((Valid (s,J)) . v) = FALSE by Th10;
then (Valid (s,J)) . v = TRUE by MARGREL1:11;
then (Valid (s,J)) . w = TRUE by A20, A21, QC_LANG3:7;
then 'not' ((Valid (s,J)) . w) = FALSE by MARGREL1:11;
hence (Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w by A23, Th10; :: thesis: verum

end;

now :: thesis: ( (Valid (('not' s),J)) . v = TRUE implies (Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w )

assume A24: (Valid (('not' s),J)) . v = TRUE ; :: thesis: (Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w
then 'not' ((Valid (s,J)) . v) = TRUE by Th10;
then (Valid (s,J)) . v = FALSE by MARGREL1:11;
then (Valid (s,J)) . w = FALSE by A20, A21, QC_LANG3:7;
then 'not' ((Valid (s,J)) . w) = TRUE by MARGREL1:11;
hence (Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w by A24, Th10; :: thesis: verum

end;

hence (Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w by A22, XBOOLEAN:def 3; :: thesis: verum

end;

end;

thus ( S₁[s] & S₁[t] implies S₁[s '&' t] ) :: thesis: ( S₁[s] implies S₁[ All (y,s)] )

proof

assume that
A25: ( not x in still_not-bound_in s implies for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid (s,J)) . v = (Valid (s,J)) . w ) and
A26: ( not x in still_not-bound_in t implies for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid (t,J)) . v = (Valid (t,J)) . w ) and
A27: not x in still_not-bound_in (s '&' t) ; :: thesis: for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w
A28: not x in (still_not-bound_in s) \/ (still_not-bound_in t) by A27, QC_LANG3:10;
thus for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w :: thesis: verum

proof

let v, w be Element of Valuations_in (Al,A); :: thesis: ( ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) implies (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w )
assume A29: for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ; :: thesis: (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w

A30: now :: thesis: ( (Valid ((s '&' t),J)) . v = FALSE implies (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w )

assume A31: (Valid ((s '&' t),J)) . v = FALSE ; :: thesis: (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w

A32: now :: thesis: ( (Valid (s,J)) . v = FALSE implies (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w )

assume (Valid (s,J)) . v = FALSE ; :: thesis: (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w
then (Valid (s,J)) . w = FALSE by A25, A28, A29, XBOOLE_0:def 3;
then ((Valid (s,J)) . w) '&' ((Valid (t,J)) . w) = FALSE by MARGREL1:12;
hence (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w by A31, Th12; :: thesis: verum

end;

A33: now :: thesis: ( (Valid (t,J)) . v = FALSE implies (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w )

assume (Valid (t,J)) . v = FALSE ; :: thesis: (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w
then (Valid (t,J)) . w = FALSE by A26, A28, A29, XBOOLE_0:def 3;
then ((Valid (s,J)) . w) '&' ((Valid (t,J)) . w) = FALSE by MARGREL1:12;
hence (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w by A31, Th12; :: thesis: verum

end;

((Valid (s,J)) . v) '&' ((Valid (t,J)) . v) = FALSE by A31, Th12;
hence (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w by A32, A33, MARGREL1:12; :: thesis: verum

end;

now :: thesis: ( (Valid ((s '&' t),J)) . v = TRUE implies (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w )

assume A34: (Valid ((s '&' t),J)) . v = TRUE ; :: thesis: (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w
then A35: ((Valid (s,J)) . v) '&' ((Valid (t,J)) . v) = TRUE by Th12;
then (Valid (t,J)) . v = TRUE by MARGREL1:12;
then A36: (Valid (t,J)) . w = TRUE by A26, A28, A29, XBOOLE_0:def 3;
(Valid (s,J)) . v = TRUE by A35, MARGREL1:12;
then (Valid (s,J)) . w = TRUE by A25, A28, A29, XBOOLE_0:def 3;
then ((Valid (s,J)) . w) '&' ((Valid (t,J)) . w) = TRUE by A36;
hence (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w by A34, Th12; :: thesis: verum

end;

hence (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w by A30, XBOOLEAN:def 3; :: thesis: verum

end;

end;

thus ( S₁[s] implies S₁[ All (y,s)] ) :: thesis: verum

proof

assume that
A37: ( not x in still_not-bound_in s implies for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid (s,J)) . v = (Valid (s,J)) . w ) and
A38: not x in still_not-bound_in (All (y,s)) ; :: thesis: for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w
A39: not x in (still_not-bound_in s) \ {y} by A38, QC_LANG3:12;
thus for v, w being Element of Valuations_in (Al,A) st ( for z being bound_QC-variable of Al st x <> z holds
w . z = v . z ) holds
(Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w :: thesis: verum

proof

let v, w be Element of Valuations_in (Al,A); :: thesis: ( ( for z being bound_QC-variable of Al st x <> z holds
w . z = v . z ) implies (Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w )
assume A40: for z being bound_QC-variable of Al st x <> z holds
w . z = v . z ; :: thesis: (Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w

A41: now :: thesis: ( (Valid ((All (y,s)),J)) . v = FALSE implies (Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w )

assume A42: (Valid ((All (y,s)),J)) . v = FALSE ; :: thesis: (Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w
then (FOR_ALL (y,(Valid (s,J)))) . v = FALSE by Lm1;
then consider v1 being Element of Valuations_in (Al,A) such that
A43: (Valid (s,J)) . v1 = FALSE and
A44: for z being bound_QC-variable of Al st y <> z holds
v1 . z = v . z by Th2;

A45: now :: thesis: ( not x in still_not-bound_in s implies ex v2 being Element of Valuations_in (Al,A) st
( (Valid (s,J)) . v2 = FALSE & ( for z being bound_QC-variable of Al st y <> z holds
v2 . z = w . z ) ) )

assume A46: not x in still_not-bound_in s ; :: thesis: ex v2 being Element of Valuations_in (Al,A) st
( (Valid (s,J)) . v2 = FALSE & ( for z being bound_QC-variable of Al st y <> z holds
v2 . z = w . z ) )
consider v2 being Element of Valuations_in (Al,A) such that
A47: ( ( for z being bound_QC-variable of Al st z <> y holds
v2 . z = w . z ) & v2 . y = v1 . y ) by Lm3;
take v2 = v2; :: thesis: ( (Valid (s,J)) . v2 = FALSE & ( for z being bound_QC-variable of Al st y <> z holds
v2 . z = w . z ) )
for z being bound_QC-variable of Al st x <> z holds
v2 . z = v1 . z

proof

let z be bound_QC-variable of Al; :: thesis: ( x <> z implies v2 . z = v1 . z )
assume A48: x <> z ; :: thesis: v2 . z = v1 . z

now :: thesis: ( z <> y implies v2 . z = v1 . z )

assume A49: z <> y ; :: thesis: v2 . z = v1 . z
hence v2 . z = w . z by A47
.= v . z by A40, A48
.= v1 . z by A44, A49 ;
:: thesis: verum

end;

hence v2 . z = v1 . z by A47; :: thesis: verum

end;

hence (Valid (s,J)) . v2 = FALSE by A37, A43, A46; :: thesis: for z being bound_QC-variable of Al st y <> z holds
v2 . z = w . z
thus for z being bound_QC-variable of Al st y <> z holds
v2 . z = w . z by A47; :: thesis: verum

end;

now :: thesis: ( x in {y} implies ex v2 being Element of Valuations_in (Al,A) st
( (Valid (s,J)) . v2 = FALSE & ( for z being bound_QC-variable of Al st y <> z holds
v2 . z = w . z ) ) )

assume A50: x in {y} ; :: thesis: ex v2 being Element of Valuations_in (Al,A) st
( (Valid (s,J)) . v2 = FALSE & ( for z being bound_QC-variable of Al st y <> z holds
v2 . z = w . z ) )
take v2 = v1; :: thesis: ( (Valid (s,J)) . v2 = FALSE & ( for z being bound_QC-variable of Al st y <> z holds
v2 . z = w . z ) )
thus (Valid (s,J)) . v2 = FALSE by A43; :: thesis: for z being bound_QC-variable of Al st y <> z holds
v2 . z = w . z
for z being bound_QC-variable of Al st y <> z holds
v1 . z = w . z

proof

let z be bound_QC-variable of Al; :: thesis: ( y <> z implies v1 . z = w . z )
assume A51: y <> z ; :: thesis: v1 . z = w . z
then A52: x <> z by A50, TARSKI:def 1;
thus v1 . z = v . z by A44, A51
.= w . z by A40, A52 ; :: thesis: verum

end;

hence for z being bound_QC-variable of Al st y <> z holds
v2 . z = w . z ; :: thesis: verum

end;

then (FOR_ALL (y,(Valid (s,J)))) . w = FALSE by A39, A45, Th2, XBOOLE_0:def 5;
hence (Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w by A42, Lm1; :: thesis: verum

end;

now :: thesis: ( (Valid ((All (y,s)),J)) . v = TRUE implies (Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w )

assume A53: (Valid ((All (y,s)),J)) . v = TRUE ; :: thesis: (Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w
then A54: (FOR_ALL (y,(Valid (s,J)))) . v = TRUE by Lm1;
for v1 being Element of Valuations_in (Al,A) st ( for z being bound_QC-variable of Al st y <> z holds
v1 . z = w . z ) holds
(Valid (s,J)) . v1 = TRUE

proof

let v1 be Element of Valuations_in (Al,A); :: thesis: ( ( for z being bound_QC-variable of Al st y <> z holds
v1 . z = w . z ) implies (Valid (s,J)) . v1 = TRUE )
assume A55: for z being bound_QC-variable of Al st y <> z holds
v1 . z = w . z ; :: thesis: (Valid (s,J)) . v1 = TRUE

A56: now :: thesis: ( not x in still_not-bound_in s implies (Valid (s,J)) . v1 = TRUE )

assume A57: not x in still_not-bound_in s ; :: thesis: (Valid (s,J)) . v1 = TRUE
consider v2 being Element of Valuations_in (Al,A) such that
A58: ( ( for z being bound_QC-variable of Al st z <> y holds
v2 . z = v . z ) & v2 . y = v1 . y ) by Lm3;
A59: for z being bound_QC-variable of Al st x <> z holds
v2 . z = v1 . z

proof

let z be bound_QC-variable of Al; :: thesis: ( x <> z implies v2 . z = v1 . z )
assume A60: x <> z ; :: thesis: v2 . z = v1 . z

now :: thesis: ( z <> y implies v2 . z = v1 . z )

assume A61: z <> y ; :: thesis: v2 . z = v1 . z
hence v2 . z = v . z by A58
.= w . z by A40, A60
.= v1 . z by A55, A61 ;
:: thesis: verum

end;

hence v2 . z = v1 . z by A58; :: thesis: verum

end;

(Valid (s,J)) . v2 = TRUE by A54, A58, Th3;
hence (Valid (s,J)) . v1 = TRUE by A37, A57, A59; :: thesis: verum

end;

now :: thesis: ( x in {y} implies (Valid (s,J)) . v1 = TRUE )

assume x in {y} ; :: thesis: (Valid (s,J)) . v1 = TRUE
then A62: x = y by TARSKI:def 1;
for z being bound_QC-variable of Al st y <> z holds
v1 . z = v . z

proof

let z be bound_QC-variable of Al; :: thesis: ( y <> z implies v1 . z = v . z )
assume A63: y <> z ; :: thesis: v1 . z = v . z
hence v . z = w . z by A40, A62
.= v1 . z by A55, A63 ;
:: thesis: verum

end;

hence (Valid (s,J)) . v1 = TRUE by A54, Th3; :: thesis: verum

end;

hence (Valid (s,J)) . v1 = TRUE by A39, A56, XBOOLE_0:def 5; :: thesis: verum

end;

then (FOR_ALL (y,(Valid (s,J)))) . w = TRUE by Th3;
hence (Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w by A53, Lm1; :: thesis: verum

end;

hence (Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w by A41, XBOOLEAN:def 3; :: thesis: verum

end;

end;

end;

for s being Element of CQC-WFF Al holds S₁[s] from CQC_LANG:sch 1(A1);
hence ( not x in still_not-bound_in p implies for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = v . y ) holds
(Valid (p,J)) . v = (Valid (p,J)) . w ) ; :: thesis: verum