let X be Subset of CQC-WFF; :: thesis: for p, q being Element of CQC-WFF st X |- p & X |- p => q holds
X |- q
let p, q be Element of CQC-WFF ; :: 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 Def9;
then q in Cn X by Th32;
hence X |- q by Def9; :: thesis: verum