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

proof

assume A1: All (x,p) is Element of CQC-WFF A ; :: thesis: p is Element of CQC-WFF A
then Fixed (All (x,p)) = {} by Th4;
then A2: Fixed p = {} by QC_LANG3:68;
Free (All (x,p)) = {} by A1, Th4;
then Free p = {} by QC_LANG3:58;
hence p is Element of CQC-WFF A by A2, Th4; :: thesis: verum

end;

assume A3: p is Element of CQC-WFF A ; :: thesis: All (x,p) is Element of CQC-WFF A
then Fixed p = {} by Th4;
then A4: Fixed (All (x,p)) = {} by QC_LANG3:68;
Free p = {} by A3, Th4;
then Free (All (x,p)) = {} by QC_LANG3:58;
hence All (x,p) is Element of CQC-WFF A by A4, Th4; :: thesis: verum