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 p '&' q is Element of CQC-WFF ; :: thesis: ( p is Element of CQC-WFF & q is Element of CQC-WFF )
then ( Free (p '&' q) = {} & Fixed (p '&' q) = {} ) by Th13;
then ( (Free p) \/ (Free q) = {} & (Fixed p) \/ (Fixed q) = {} ) by QC_LANG3:69, QC_LANG3:80;
then ( Free p = {} & Free q = {} & Fixed p = {} & Fixed q = {} ) ;
hence ( p is Element of CQC-WFF & q is Element of CQC-WFF ) by 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 ;
( Free r = {} & Free s = {} & Fixed r = {} & Fixed s = {} ) by Th13;
then ( (Free r) \/ (Free s) = {} & (Fixed r) \/ (Fixed s) = {} ) ;
then ( Free (r '&' s) = {} & Fixed (r '&' s) = {} ) by QC_LANG3:69, QC_LANG3:80;
hence p '&' q is Element of CQC-WFF by Th13; :: thesis: verum