let Al be QC-alphabet ; 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
for v being Element of Valuations_in (Al,A) holds
( J,v |= All (x,p) iff for a being Element of A holds J,v . (x | a) |= p )
let p be 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
for v being Element of Valuations_in (Al,A) holds
( J,v |= All (x,p) iff for a being Element of A holds J,v . (x | a) |= p )
let x be bound_QC-variable of Al; for A being non empty set
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) holds
( J,v |= All (x,p) iff for a being Element of A holds J,v . (x | a) |= p )
let A be non empty set ; for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) holds
( J,v |= All (x,p) iff for a being Element of A holds J,v . (x | a) |= p )
let J be interpretation of Al,A; for v being Element of Valuations_in (Al,A) holds
( J,v |= All (x,p) iff for a being Element of A holds J,v . (x | a) |= p )
let v be Element of Valuations_in (Al,A); ( J,v |= All (x,p) iff for a being Element of A holds J,v . (x | a) |= p )
thus
( J,v |= All (x,p) implies for a being Element of A holds J,v . (x | a) |= p )
( ( for a being Element of A holds J,v . (x | a) |= p ) implies J,v |= All (x,p) )
thus
( ( for a being Element of A holds J,v . (x | a) |= p ) implies J,v |= All (x,p) )
verum