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 A1: p is valid ; :: thesis: X |- p
A2: p in TAUT by A1, Lm13;
A3: TAUT c= Cn X by Th36, Th74;
thus X |- p by A2, A3, Def9; :: thesis: verum