let X be Subset of CQC-WFF ; :: thesis: for p being Element of CQC-WFF st p is valid holds
X |- p
let p be Element of CQC-WFF ; :: thesis: ( p is valid implies X |- p )
assume p is valid ; :: thesis: X |- p
then ( p in TAUT & TAUT c= Cn X ) by Lm13, Th75;
hence X |- p by Def9; :: thesis: verum