let p be Element of QC-WFF ; :: thesis: ( p is Element of CQC-WFF iff ( Fixed p = {} & Free p = {} ) )
thus ( p is Element of CQC-WFF implies ( Fixed p = {} & Free p = {} ) ) :: thesis: ( Fixed p = {} & Free p = {} implies p is Element of CQC-WFF )

proof

assume p is Element of CQC-WFF ; :: thesis: ( Fixed p = {} & Free p = {} )
then p in CQC-WFF ;
then ex s being QC-formula st
( s = p & Fixed s = {} & Free s = {} ) ;
hence ( Fixed p = {} & Free p = {} ) ; :: thesis: verum

end;

assume ( Fixed p = {} & Free p = {} ) ; :: thesis: p is Element of CQC-WFF
then p in CQC-WFF ;
hence p is Element of CQC-WFF ; :: thesis: verum