let A be non empty set ; :: thesis: for x being bound_QC-variable
for p, q being Element of CQC-WFF
for J being interpretation of 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; :: thesis: for p, q being Element of CQC-WFF
for J being interpretation of 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 ; :: thesis: for J being interpretation of A st J |= p => q & not x in still_not-bound_in p holds
J |= p => (All (x,q))
let J be interpretation of 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 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 A; :: according to VALUAT_1:def 8 :: thesis: J,u |= p => (All (x,q))

now

assume A3: J,u |= p ; :: thesis: J,u |= All (x,q)

now

let w be Element of Valuations_in A; :: thesis: ( ( for y being bound_QC-variable st x <> y holds
w . y = u . y ) implies J,w |= q )
assume for y being bound_QC-variable st x <> y holds
w . y = u . y ; :: thesis: J,w |= q
then A4: J,w |= p by A2, A3, Th40;
J,w |= p => q by A1;
hence J,w |= q by A4, Th36; :: thesis: verum

end;

hence J,u |= All (x,q) by Th41; :: thesis: verum

end;

hence J,u |= p => (All (x,q)) by Th36; :: thesis: verum