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 )

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

p in {p} by TARSKI:def 1;
hence ( X |- {p} implies X |- p ) ; :: thesis: verum

end;

thus ( X |- p implies X |- {p} ) by TARSKI:def 1; :: thesis: verum