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