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