let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A
for X being Subset of (CQC-WFF A) st p |-| q & X |- p holds
X |- q
let p, q be Element of CQC-WFF A; :: thesis: for X being Subset of (CQC-WFF A) st p |-| q & X |- p holds
X |- q
let X be Subset of (CQC-WFF A); :: thesis: ( p |-| q & X |- p implies X |- q )
assume that
A1: p |-| q and
A2: X |- p ; :: thesis: X |- q
A3: X |- {p} by A2, Th10;
{p} |-| {q} by A1, Th29;
then X |- {q} by A3, Th27;
hence X |- q by Th10; :: thesis: verum