let p, q be Element of QC-WFF ; :: thesis: ( p '&' q is Element of CQC-WFF iff ( p is Element of CQC-WFF & q is Element of CQC-WFF ) )
thus ( p '&' q is Element of CQC-WFF implies ( p is Element of CQC-WFF & q is Element of CQC-WFF ) ) :: thesis: ( p is Element of CQC-WFF & q is Element of CQC-WFF implies p '&' q is Element of CQC-WFF )

proof

assume A1: p '&' q is Element of CQC-WFF ; :: thesis: ( p is Element of CQC-WFF & q is Element of CQC-WFF )
then Fixed (p '&' q) = {} by Th13;
then A2: (Fixed p) \/ (Fixed q) = {} by QC_LANG3:80;
then A3: Fixed p = {} ;
Free (p '&' q) = {} by A1, Th13;
then A4: (Free p) \/ (Free q) = {} by QC_LANG3:69;
then Free p = {} ;
hence ( p is Element of CQC-WFF & q is Element of CQC-WFF ) by A4, A2, A3, Th13; :: thesis: verum

end;

assume ( p is Element of CQC-WFF & q is Element of CQC-WFF ) ; :: thesis: p '&' q is Element of CQC-WFF
then reconsider r = p, s = q as Element of CQC-WFF ;
Fixed r = {} by Th13;
then (Fixed r) \/ (Fixed s) = {} by Th13;
then A5: Fixed (r '&' s) = {} by QC_LANG3:80;
Free r = {} by Th13;
then (Free r) \/ (Free s) = {} by Th13;
then Free (r '&' s) = {} by QC_LANG3:69;
hence p '&' q is Element of CQC-WFF by A5, Th13; :: thesis: verum