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 '&' q holds
( X |- p & X |- q )
let p, q be Element of CQC-WFF A; :: thesis: for X being Subset of (CQC-WFF A) st X |- p '&' q holds
( X |- p & X |- q )
let X be Subset of (CQC-WFF A); :: thesis: ( X |- p '&' q implies ( X |- p & X |- q ) )
assume X |- p '&' q ; :: thesis: ( X |- p & X |- q )
then A1: X |- {(p '&' q)} by Th10;
{p,q} |-| {(p '&' q)} by Th31;
then A2: X |- {p,q} by A1, Th27;
p in {p,q} by TARSKI:def 2;
hence X |- p by A2; :: thesis: X |- q
q in {p,q} by TARSKI:def 2;
hence X |- q by A2; :: thesis: verum