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

A1: now :: thesis: ( X |- p implies X |- {p} )

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

end;

now :: thesis: ( X |- {p} implies X |- p )

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