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

A1: now :: thesis: ( |- X implies X c= TAUT A )

assume A2: |- X ; :: thesis: X c= TAUT A

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

let p be Element of CQC-WFF A; :: thesis: ( p in X implies p in TAUT A )
assume p in X ; :: thesis: p in TAUT A
then p is valid by A2, Def3;
hence p in TAUT A by CQC_THE1:def 10; :: thesis: verum

end;

hence X c= TAUT A by SUBSET_1:2; :: thesis: verum

end;

now :: thesis: ( X c= TAUT A implies |- X )

assume X c= TAUT A ; :: thesis: |- X
then for p being Element of CQC-WFF A st p in X holds
p is valid by CQC_THE1:def 10;
hence |- X by Def3; :: thesis: verum

end;

hence ( |- X iff X c= TAUT A ) by A1; :: thesis: verum