let Al be QC-alphabet ; :: thesis: for X being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al st p is valid holds
X |- p
let X be Subset of (CQC-WFF Al); :: thesis: for p being Element of CQC-WFF Al st p is valid holds
X |- p
let p be Element of CQC-WFF Al; :: thesis: ( p is valid implies X |- p )
assume p is valid ; :: thesis: X |- p
then A1: p in TAUT Al by Lm13;
TAUT Al c= Cn X by Th15, Th38;
hence X |- p by A1, Def8; :: thesis: verum