let A be QC-alphabet ; :: thesis: for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 & CQC_Sub S1 is Element of CQC-WFF A & CQC_Sub S2 is Element of CQC-WFF A holds
CQC_Sub (Sub_& (S1,S2)) is Element of CQC-WFF A
let S1, S2 be Element of QC-Sub-WFF A; :: thesis: ( S1 `2 = S2 `2 & CQC_Sub S1 is Element of CQC-WFF A & CQC_Sub S2 is Element of CQC-WFF A implies CQC_Sub (Sub_& (S1,S2)) is Element of CQC-WFF A )
assume A1: ( S1 `2 = S2 `2 & CQC_Sub S1 is Element of CQC-WFF A & CQC_Sub S2 is Element of CQC-WFF A ) ; :: thesis: CQC_Sub (Sub_& (S1,S2)) is Element of CQC-WFF A
( S1 `2 = S2 `2 implies CQC_Sub (Sub_& (S1,S2)) = (CQC_Sub S1) '&' (CQC_Sub S2) ) by Th31;
hence CQC_Sub (Sub_& (S1,S2)) is Element of CQC-WFF A by A1, CQC_LANG:9; :: thesis: verum