let Al be QC-alphabet ; :: thesis:
let p be Element of CQC-WFF Al; :: thesis:
let x, y be bound_QC-variable of Al; :: thesis:
let f be FinSequence of CQC-WFF Al; :: thesis:
assume that
A1: ( Suc f = p . (x,y) & Ant f |= Suc f ) and
A2: not y in still_not-bound_in (Ant f) and
A3: not y in still_not-bound_in (All (x,p)) ; :: thesis:
let A be non empty set ; :: according to CALCUL_1:def 15 :: thesis:
let J be interpretation of Al,A; :: thesis:
let v be Element of Valuations_in (Al,A); :: thesis:
assume A4: J,v |= Ant f ; :: thesis:
for a being Element of A holds J,v . (x | a) |= p

proof

let a be Element of A; :: thesis:
(v . (y | a)) | (still_not-bound_in (Ant f)) = v | (still_not-bound_in (Ant f)) by A2, Th26;
then J,v . (y | a) |= Ant f by A4, Th27;
then J,v . (y | a) |= p . (x,y) by A1;
then ex a1 being Element of A st
( (v . (y | a)) . y = a1 & J,(v . (y | a)) . (x | a1) |= p ) by Th24;
then A5: J,(v . (y | a)) . (x | a) |= p by SUBLEMMA:49;
((v . (y | a)) . (x | a)) | (still_not-bound_in p) = (v . (x | a)) | (still_not-bound_in p) by A3, Th28;
hence J,v . (x | a) |= p by A5, SUBLEMMA:68; :: thesis:

end;

hence J,v |= All (x,p) by SUBLEMMA:50; :: thesis: