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

A1: now

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

now

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

end;

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

end;

now

assume X c= TAUT ; :: thesis: |- X
then for p being Element of CQC-WFF 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 ) by A1; :: thesis: verum