let X, Y be Subset of CQC-WFF ; :: thesis: ( X |- Y iff Y c= Cn X )

A1: now

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

now

let p be set ; :: thesis: ( p in Y implies p in Cn X )
assume A3: p in Y ; :: thesis: p in Cn X
then reconsider p' = p as Element of CQC-WFF ;
X |- p' by A2, A3, Def2;
hence p in Cn X by CQC_THE1:def 9; :: thesis: verum

end;

hence Y c= Cn X by TARSKI:def 3; :: thesis: verum

end;

now

assume Y c= Cn X ; :: thesis: X |- Y
then for p being Element of CQC-WFF st p in Y holds
X |- p by CQC_THE1:def 9;
hence X |- Y by Def2; :: thesis: verum

end;

hence ( X |- Y iff Y c= Cn X ) by A1; :: thesis: verum