let x be bound_QC-variable; :: thesis: for p being Element of QC-WFF holds
( All x,p is Element of CQC-WFF iff p is Element of CQC-WFF )
let p be Element of QC-WFF ; :: thesis: ( All x,p is Element of CQC-WFF iff p is Element of CQC-WFF )
thus ( All x,p is Element of CQC-WFF implies p is Element of CQC-WFF ) :: thesis: ( p is Element of CQC-WFF implies All x,p is Element of CQC-WFF )

proof

assume All x,p is Element of CQC-WFF ; :: thesis: p is Element of CQC-WFF
then ( Free (All x,p) = {} & Fixed (All x,p) = {} ) by Th13;
then ( Free p = {} & Fixed p = {} ) by QC_LANG3:70, QC_LANG3:81;
hence p is Element of CQC-WFF by Th13; :: thesis: verum

end;

assume p is Element of CQC-WFF ; :: thesis: All x,p is Element of CQC-WFF
then ( Free p = {} & Fixed p = {} ) by Th13;
then ( Free (All x,p) = {} & Fixed (All x,p) = {} ) by QC_LANG3:70, QC_LANG3:81;
hence All x,p is Element of CQC-WFF by Th13; :: thesis: verum