let Al be QC-alphabet ; :: thesis: for X being Subset of (CQC-WFF Al)
for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al st X |- p => q & not x in still_not-bound_in p holds
X |- p => (All (x,q))
let X be Subset of (CQC-WFF Al); :: thesis: for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al st X |- p => q & not x in still_not-bound_in p holds
X |- p => (All (x,q))
let p, q be Element of CQC-WFF Al; :: thesis: for x being bound_QC-variable of Al st X |- p => q & not x in still_not-bound_in p holds
X |- p => (All (x,q))
let x be bound_QC-variable of Al; :: thesis: ( X |- p => q & not x in still_not-bound_in p implies X |- p => (All (x,q)) )
assume that
A1: X |- p => q and
A2: not x in still_not-bound_in p ; :: thesis: X |- p => (All (x,q))
p => q in Cn X by A1, Def8;
then p => (All (x,q)) in Cn X by A2, Th13;
hence X |- p => (All (x,q)) by Def8; :: thesis: verum