let A be QC-alphabet ; :: thesis: for p, q being Element of QC-WFF A holds
( p '&' q is Element of CQC-WFF A iff ( p is Element of CQC-WFF A & q is Element of CQC-WFF A ) )
let p, q be Element of QC-WFF A; :: thesis: ( p '&' q is Element of CQC-WFF A iff ( p is Element of CQC-WFF A & q is Element of CQC-WFF A ) )
thus ( p '&' q is Element of CQC-WFF A implies ( p is Element of CQC-WFF A & q is Element of CQC-WFF A ) ) :: thesis: ( p is Element of CQC-WFF A & q is Element of CQC-WFF A implies p '&' q is Element of CQC-WFF A )
proof
assume A1: p '&' q is Element of CQC-WFF A ; :: thesis: ( p is Element of CQC-WFF A & q is Element of CQC-WFF A )
then Fixed (p '&' q) = {} by Th4;
then A2: (Fixed p) \/ (Fixed q) = {} by QC_LANG3:67;
then A3: Fixed p = {} ;
Free (p '&' q) = {} by A1, Th4;
then A4: (Free p) \/ (Free q) = {} by QC_LANG3:57;
then Free p = {} ;
hence ( p is Element of CQC-WFF A & q is Element of CQC-WFF A ) by A4, A2, A3, Th4; :: thesis: verum
end;
assume ( p is Element of CQC-WFF A & q is Element of CQC-WFF A ) ; :: thesis: p '&' q is Element of CQC-WFF A
then reconsider r = p, s = q as Element of CQC-WFF A ;
Fixed r = {} by Th4;
then (Fixed r) \/ (Fixed s) = {} by Th4;
then A5: Fixed (r '&' s) = {} by QC_LANG3:67;
Free r = {} by Th4;
then (Free r) \/ (Free s) = {} by Th4;
then Free (r '&' s) = {} by QC_LANG3:57;
hence p '&' q is Element of CQC-WFF A by A5, Th4; :: thesis: verum