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

hereby :: thesis: ( Y c= Cn X implies X |- Y )

assume A1: X |- Y ; :: thesis: Y c= Cn X

now :: thesis: for p being object st p in Y holds
p in Cn X

let p be object ; :: thesis: ( p in Y implies p in Cn X )
assume A2: p in Y ; :: thesis: p in Cn X
then reconsider p9 = p as Element of CQC-WFF A ;
X |- p9 by A1, A2;
hence p in Cn X by CQC_THE1:def 8; :: thesis: verum

end;

hence Y c= Cn X ; :: thesis: verum

end;

thus ( Y c= Cn X implies X |- Y ) by CQC_THE1:def 8; :: thesis: verum