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 Element of 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 Element of 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 Element of 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 Element of 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;
A10: i in NAT by ORDINAL1:def 12;
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 Element of NAT : ( 1 <= i2 & i2 <= len ll & ll . i2 in bound_QC-variables Al ) } by QC_LANG3:def 1;
hence ll . i <> x by A8, A10, A9; :: thesis: verum

end;

then A11: 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, A11, Def3; :: thesis: verum

end;

assume A12: (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 A13: v *' ll in J . P by Def4;
len (w *' ll) = k by Def3;
then w *' ll in J . P by A13, 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 A12, Lm1; :: thesis: verum

end;

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

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

A15: 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 A16: ( 1 <= i & i <= len (v *' ll) ) ; :: thesis: (v *' ll) . i = (w *' ll) . i
A17: len (v *' ll) = len ll by A14, CARD_1:def 7;
then i in dom ll by A16, 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 Element of 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 A16, A17; :: thesis: verum

end;

then A18: w . z = v . z by A4;
(v *' ll) . i = v . (ll . i) by A14, A16, Def3;
hence (v *' ll) . i = (w *' ll) . i by A14, A16, A18, Def3; :: thesis: verum

end;

assume A19: (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 A20: not v *' ll in J . P by Def4;
len (w *' ll) = k by Def3;
then not w *' ll in J . P by A20, A14, A15, FINSEQ_1:14;
then (ll 'in' (J . P)) . w = FALSE by Def4;
hence (Valid ((P ! ll),J)) . v = (Valid ((P ! ll),J)) . w by A19, 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 A21: ( ( 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 A22: 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

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

assume A24: (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 A21, A22, 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 A24, Th10; :: thesis: verum

end;

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

assume A25: (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 A21, A22, 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 A25, Th10; :: thesis: verum

end;

hence (Valid (('not' s),J)) . v = (Valid (('not' s),J)) . w by A23, 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
A26: ( 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
A27: ( 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
A28: 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
A29: not x in (still_not-bound_in s) \/ (still_not-bound_in t) by A28, 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 A30: 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

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

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

A33: 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 A26, A29, A30, 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 A32, Th12; :: thesis: verum

end;

A34: 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 A27, A29, A30, 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 A32, Th12; :: thesis: verum

end;

((Valid (s,J)) . v) '&' ((Valid (t,J)) . v) = FALSE by A32, Th12;
hence (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w by A33, A34, 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 A35: (Valid ((s '&' t),J)) . v = TRUE ; :: thesis: (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w
then A36: ((Valid (s,J)) . v) '&' ((Valid (t,J)) . v) = TRUE by Th12;
then (Valid (t,J)) . v = TRUE by MARGREL1:12;
then A37: (Valid (t,J)) . w = TRUE by A27, A29, A30, XBOOLE_0:def 3;
(Valid (s,J)) . v = TRUE by A36, MARGREL1:12;
then (Valid (s,J)) . w = TRUE by A26, A29, A30, XBOOLE_0:def 3;
then ((Valid (s,J)) . w) '&' ((Valid (t,J)) . w) = TRUE by A37;
hence (Valid ((s '&' t),J)) . v = (Valid ((s '&' t),J)) . w by A35, Th12; :: thesis: verum

end;

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

end;

end;

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

proof

assume that
A38: ( 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
A39: 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
A40: not x in (still_not-bound_in s) \ {y} by A39, 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 A41: 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

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

assume A43: (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
A44: (Valid (s,J)) . v1 = FALSE and
A45: for z being bound_QC-variable of Al st y <> z holds
v1 . z = v . z by Th2;

A46: 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 A47: 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
A48: ( ( 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 A49: x <> z ; :: thesis: v2 . z = v1 . z

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

assume A50: z <> y ; :: thesis: v2 . z = v1 . z
hence v2 . z = w . z by A48
.= v . z by A41, A49
.= v1 . z by A45, A50 ;
:: thesis: verum

end;

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

end;

hence (Valid (s,J)) . v2 = FALSE by A38, A44, A47; :: 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 A48; :: 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 A51: 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 A44; :: 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 A52: y <> z ; :: thesis: v1 . z = w . z
then A53: x <> z by A51, TARSKI:def 1;
thus v1 . z = v . z by A45, A52
.= w . z by A41, A53 ; :: 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 A40, A46, Th2, XBOOLE_0:def 5;
hence (Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w by A43, 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 A54: (Valid ((All (y,s)),J)) . v = TRUE ; :: thesis: (Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w
then A55: (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 A56: for z being bound_QC-variable of Al st y <> z holds
v1 . z = w . z ; :: thesis: (Valid (s,J)) . v1 = TRUE

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

assume A58: 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
A59: ( ( for z being bound_QC-variable of Al st z <> y holds
v2 . z = v . z ) & v2 . y = v1 . y ) by Lm3;
A60: 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 A61: x <> z ; :: thesis: v2 . z = v1 . z

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

assume A62: z <> y ; :: thesis: v2 . z = v1 . z
hence v2 . z = v . z by A59
.= w . z by A41, A61
.= v1 . z by A56, A62 ;
:: thesis: verum

end;

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

end;

(Valid (s,J)) . v2 = TRUE by A55, A59, Th3;
hence (Valid (s,J)) . v1 = TRUE by A38, A58, A60; :: 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 A63: 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 A64: y <> z ; :: thesis: v1 . z = v . z
hence v . z = w . z by A41, A63
.= v1 . z by A56, A64 ;
:: thesis: verum

end;

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

end;

hence (Valid (s,J)) . v1 = TRUE by A40, A57, 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 A54, Lm1; :: thesis: verum

end;

hence (Valid ((All (y,s)),J)) . v = (Valid ((All (y,s)),J)) . w by A42, 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