let Al be QC-alphabet ; :: thesis: for A being non empty set
for x being bound_QC-variable of Al
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A st J |= p => q & not x in still_not-bound_in p holds
J |= p => (All (x,q))
let A be non empty set ; :: thesis: for x being bound_QC-variable of Al
for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A st J |= p => q & not x in still_not-bound_in p holds
J |= p => (All (x,q))
let x be bound_QC-variable of Al; :: thesis: for p, q being Element of CQC-WFF Al
for J being interpretation of Al,A st J |= p => q & not x in still_not-bound_in p holds
J |= p => (All (x,q))
let p, q be Element of CQC-WFF Al; :: thesis: for J being interpretation of Al,A st J |= p => q & not x in still_not-bound_in p holds
J |= p => (All (x,q))
let J be interpretation of Al,A; :: thesis: ( J |= p => q & not x in still_not-bound_in p implies J |= p => (All (x,q)) )
assume that
A1: for v being Element of Valuations_in (Al,A) holds J,v |= p => q and
A2: not x in still_not-bound_in p ; :: according to VALUAT_1:def 8 :: thesis: J |= p => (All (x,q))
let u be Element of Valuations_in (Al,A); :: according to VALUAT_1:def 8 :: thesis: J,u |= p => (All (x,q))
now :: thesis: ( J,u |= p implies J,u |= All (x,q) )
assume A3: J,u |= p ; :: thesis: J,u |= All (x,q)
now :: thesis: for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds
w . y = u . y ) holds
J,w |= q
let w be Element of Valuations_in (Al,A); :: thesis: ( ( for y being bound_QC-variable of Al st x <> y holds
w . y = u . y ) implies J,w |= q )
assume for y being bound_QC-variable of Al st x <> y holds
w . y = u . y ; :: thesis: J,w |= q
then A4: J,w |= p by A2, A3, Th28;
J,w |= p => q by A1;
hence J,w |= q by A4, Th24; :: thesis: verum
end;
hence J,u |= All (x,q) by Th29; :: thesis: verum
end;
hence J,u |= p => (All (x,q)) by Th24; :: thesis: verum