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 A1: ( X |- p & X |- p => q ) ; :: thesis: X |- q
A2: ( p in Cn X & p => q in Cn X ) by A1, Def9;
A3: q in Cn X by A2, Th32;
thus X |- q by A3, Def9; :: thesis: verum