let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for A being non empty set
for J being interpretation of Al,A st ( for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in p) = w | (still_not-bound_in p) holds
( J,v |= p iff J,w |= p ) ) holds
for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in (All (x,p))) = w | (still_not-bound_in (All (x,p))) holds
( J,v |= All (x,p) iff J,w |= All (x,p) )
let p be Element of CQC-WFF Al; :: thesis: for x being bound_QC-variable of Al
for A being non empty set
for J being interpretation of Al,A st ( for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in p) = w | (still_not-bound_in p) holds
( J,v |= p iff J,w |= p ) ) holds
for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in (All (x,p))) = w | (still_not-bound_in (All (x,p))) holds
( J,v |= All (x,p) iff J,w |= All (x,p) )
let x be bound_QC-variable of Al; :: thesis: for A being non empty set
for J being interpretation of Al,A st ( for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in p) = w | (still_not-bound_in p) holds
( J,v |= p iff J,w |= p ) ) holds
for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in (All (x,p))) = w | (still_not-bound_in (All (x,p))) holds
( J,v |= All (x,p) iff J,w |= All (x,p) )
let A be non empty set ; :: thesis: for J being interpretation of Al,A st ( for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in p) = w | (still_not-bound_in p) holds
( J,v |= p iff J,w |= p ) ) holds
for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in (All (x,p))) = w | (still_not-bound_in (All (x,p))) holds
( J,v |= All (x,p) iff J,w |= All (x,p) )
let J be interpretation of Al,A; :: thesis: ( ( for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in p) = w | (still_not-bound_in p) holds
( J,v |= p iff J,w |= p ) ) implies for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in (All (x,p))) = w | (still_not-bound_in (All (x,p))) holds
( J,v |= All (x,p) iff J,w |= All (x,p) ) )
assume A1: for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in p) = w | (still_not-bound_in p) holds
( J,v |= p iff J,w |= p ) ; :: thesis: for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in (All (x,p))) = w | (still_not-bound_in (All (x,p))) holds
( J,v |= All (x,p) iff J,w |= All (x,p) )
set X = (still_not-bound_in p) \ {x};
let v, w be Element of Valuations_in (Al,A); :: thesis: ( v | (still_not-bound_in (All (x,p))) = w | (still_not-bound_in (All (x,p))) implies ( J,v |= All (x,p) iff J,w |= All (x,p) ) )
A2: v | (still_not-bound_in (All (x,p))) = v | ((still_not-bound_in p) \ {x}) by QC_LANG3:12;
assume v | (still_not-bound_in (All (x,p))) = w | (still_not-bound_in (All (x,p))) ; :: thesis: ( J,v |= All (x,p) iff J,w |= All (x,p) )
then A3: v | ((still_not-bound_in p) \ {x}) = w | ((still_not-bound_in p) \ {x}) by A2, QC_LANG3:12;
A4: ( ( for a being Element of A holds J,w . (x | a) |= p ) implies for a being Element of A holds J,v . (x | a) |= p )

proof

assume A5: for a being Element of A holds J,w . (x | a) |= p ; :: thesis: for a being Element of A holds J,v . (x | a) |= p
let a be Element of A; :: thesis: J,v . (x | a) |= p
(v . (x | a)) | (still_not-bound_in p) = (w . (x | a)) | (still_not-bound_in p) by A3, Th66;
then ( J,v . (x | a) |= p iff J,w . (x | a) |= p ) by A1;
hence J,v . (x | a) |= p by A5; :: thesis: verum

end;

( ( for a being Element of A holds J,v . (x | a) |= p ) implies for a being Element of A holds J,w . (x | a) |= p )

proof

assume A6: for a being Element of A holds J,v . (x | a) |= p ; :: thesis: for a being Element of A holds J,w . (x | a) |= p
let a be Element of A; :: thesis: J,w . (x | a) |= p
(v . (x | a)) | (still_not-bound_in p) = (w . (x | a)) | (still_not-bound_in p) by A3, Th66;
then ( J,v . (x | a) |= p iff J,w . (x | a) |= p ) by A1;
hence J,w . (x | a) |= p by A6; :: thesis: verum

end;

hence ( J,v |= All (x,p) iff J,w |= All (x,p) ) by A4, Th50; :: thesis: verum