let p be Element of CQC-WFF ; :: thesis: for X being Subset of CQC-WFF holds
( X |- {p} iff X |- p )
let X be Subset of CQC-WFF ; :: thesis: ( X |- {p} iff X |- p )

A1: now

assume X |- p ; :: thesis: X |- {p}
then for q being Element of CQC-WFF st q in {p} holds
X |- q by TARSKI:def 1;
hence X |- {p} by Def2; :: thesis: verum

end;

now

A2: p in {p} by TARSKI:def 1;
assume X |- {p} ; :: thesis: X |- p
hence X |- p by A2, Def2; :: thesis: verum

end;

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