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 )
assume A1: p in X ; :: thesis: X |- p
X c= Cn X by CQC_THE1:38;
hence X |- p by A1, CQC_THE1:def 9; :: thesis: verum