let p be Element of CQC-WFF ; :: thesis: for X being Subset of CQC-WFF st p in X holds
X |- p
let X be Subset of CQC-WFF ; :: thesis: ( p in X implies X |- p )
A1: X c= Cn X by CQC_THE1:38;
assume p in X ; :: thesis: X |- p
hence X |- p by A1, CQC_THE1:def 9; :: thesis: verum