let A be QC-alphabet ; :: thesis: for X being Subset of (CQC-WFF A) holds
( |- X iff {} (CQC-WFF A) |- X )
let X be Subset of (CQC-WFF A); :: thesis: ( |- X iff {} (CQC-WFF A) |- X )

hereby :: thesis: ( {} (CQC-WFF A) |- X implies |- X )

assume A1: |- X ; :: thesis: {} (CQC-WFF A) |- X

now :: thesis: for p being Element of CQC-WFF A st p in X holds
{} (CQC-WFF A) |- p

let p be Element of CQC-WFF A; :: thesis: ( p in X implies {} (CQC-WFF A) |- p )
assume p in X ; :: thesis: {} (CQC-WFF A) |- p
then p is valid by A1;
hence {} (CQC-WFF A) |- p by CQC_THE1:def 9; :: thesis: verum

end;

hence {} (CQC-WFF A) |- X ; :: thesis: verum

end;

thus ( {} (CQC-WFF A) |- X implies |- X ) by CQC_THE1:def 9; :: thesis: verum