set J = the non empty non void Signature;
set S = the non empty non void the non empty non void Signature -extension strict n PC-correct QC-correct n AL-correct AlgLangSignature over X;
take the non empty non void the non empty non void Signature -extension strict n PC-correct QC-correct n AL-correct AlgLangSignature over X ; :: thesis: ( the non empty non void the non empty non void Signature -extension strict n PC-correct QC-correct n AL-correct AlgLangSignature over X is n PC-correct & the non empty non void the non empty non void Signature -extension strict n PC-correct QC-correct n AL-correct AlgLangSignature over X is QC-correct & the non empty non void the non empty non void Signature -extension strict n PC-correct QC-correct n AL-correct AlgLangSignature over X is n AL-correct )
thus ( the non empty non void the non empty non void Signature -extension strict n PC-correct QC-correct n AL-correct AlgLangSignature over X is n PC-correct & the non empty non void the non empty non void Signature -extension strict n PC-correct QC-correct n AL-correct AlgLangSignature over X is QC-correct & the non empty non void the non empty non void Signature -extension strict n PC-correct QC-correct n AL-correct AlgLangSignature over X is n AL-correct ) ; :: thesis: verum