let Al be QC-alphabet ; :: thesis: for X being Subset of (CQC-WFF Al)
for p, q being Element of CQC-WFF Al st X |- p & X |- p => q holds
X |- q
let X be Subset of (CQC-WFF Al); :: thesis: for p, q being Element of CQC-WFF Al st X |- p & X |- p => q holds
X |- q
let p, q be Element of CQC-WFF Al; :: thesis: ( X |- p & X |- p => q implies X |- q )
assume ( X |- p & X |- p => q ) ; :: thesis: X |- q
then ( p in Cn X & p => q in Cn X ) by Def8;
then q in Cn X by Th11;
hence X |- q by Def8; :: thesis: verum