let A be QC-alphabet ; :: thesis: for p being Element of QC-WFF A holds
( p is Element of CQC-WFF A iff ( Fixed p = {} & Free p = {} ) )
let p be Element of QC-WFF A; :: thesis: ( p is Element of CQC-WFF A iff ( Fixed p = {} & Free p = {} ) )
thus ( p is Element of CQC-WFF A implies ( Fixed p = {} & Free p = {} ) ) :: thesis: ( Fixed p = {} & Free p = {} implies p is Element of CQC-WFF A )
proof
assume p is Element of CQC-WFF A ; :: thesis: ( Fixed p = {} & Free p = {} )
then p in CQC-WFF A ;
then ex s being QC-formula of A 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 A
then p in CQC-WFF A ;
hence p is Element of CQC-WFF A ; :: thesis: verum