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

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

hence
J,v |= All (x,p)
by SUBLEMMA:50; :: thesis: verum
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;(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