let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al
for x, y being bound_QC-variable of Al
for f being FinSequence of CQC-WFF Al st Suc f = p . (x,y) & Ant f |= Suc f & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) holds
Ant f |= All (x,p)

let p be Element of CQC-WFF Al; :: thesis: for x, y being bound_QC-variable of Al
for f being FinSequence of CQC-WFF Al st Suc f = p . (x,y) & Ant f |= Suc f & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) holds
Ant f |= All (x,p)

let x, y be bound_QC-variable of Al; :: thesis: for f being FinSequence of CQC-WFF Al st Suc f = p . (x,y) & Ant f |= Suc f & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) holds
Ant f |= All (x,p)

let f be FinSequence of CQC-WFF Al; :: thesis: ( Suc f = p . (x,y) & Ant f |= Suc f & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) implies Ant f |= All (x,p) )
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: Ant f |= All (x,p)
let A be non empty set ; :: according to CALCUL_1:def 15 :: thesis: for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) st J,v |= Ant f holds
J,v |= All (x,p)

let J be interpretation of Al,A; :: thesis: for v being Element of Valuations_in (Al,A) st J,v |= Ant f holds
J,v |= All (x,p)

let v be Element of Valuations_in (Al,A); :: thesis: ( J,v |= Ant f implies J,v |= All (x,p) )
assume A4: J,v |= Ant f ; :: thesis: J,v |= All (x,p)
for a being Element of A holds J,v . (x | a) |= p
proof
let a be Element of A; :: thesis: J,v . (x | a) |= p
(v . (y | a)) | () = v | () by ;
then J,v . (y | a) |= Ant f by ;
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)) | = (v . (x | a)) | by ;
hence J,v . (x | a) |= p by ; :: thesis: verum
end;
hence J,v |= All (x,p) by SUBLEMMA:50; :: thesis: verum