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)) | (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: verum

end;

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