let X be Subset of CQC-WFF ; :: thesis: for p, q being Element of CQC-WFF
for x being bound_QC-variable 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 ; :: thesis: for x being bound_QC-variable st X |- p => q & not x in still_not-bound_in p holds
X |- p => (All x,q)
let x be bound_QC-variable; :: 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)
A3: p => q in Cn X by A1, Def9;
A4: p => (All x,q) in Cn X by A2, A3, Th34;
thus X |- p => (All x,q) by A4, Def9; :: thesis: verum