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 )

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

assume A1: |- 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 A1;
hence p in TAUT A by CQC_THE1:def 10; :: thesis: verum

end;

hence X c= TAUT A ; :: thesis: verum

end;

thus ( X c= TAUT A implies |- X ) by CQC_THE1:def 10; :: thesis: verum