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 )

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

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

now :: thesis: for p being Element of CQC-WFF A st p in X holds
p is valid

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

end;

hence |- X by Def3; :: thesis: verum

end;

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

assume A3: |- 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 A3, Def3;
hence {} (CQC-WFF A) |- p by CQC_THE1:def 9; :: thesis: verum

end;

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

end;

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