let X be Subset of CQC-WFF ; :: thesis: ( |- X iff {} CQC-WFF |- X )

A1: now

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

now

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

end;

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

end;

now

assume A3: {} CQC-WFF |- X ; :: thesis: |- X

now

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

end;

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

end;

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