consider S being non empty non void strict AlgLangSignature over X such that
A1: ( S is n PC-correct & S is QC-correct & S is n AL-correct & S is J -extension ) and
( ( for i being natural number st not not i = 0 & ... & not i = 8 holds
the connectives of S . (n + i) = (sup the carrier' of J) +^ i ) & ( for x being Element of X holds
( the quantifiers of S . (1,x) = [ the carrier' of J,1,x] & the quantifiers of S . (2,x) = [ the carrier' of J,2,x] ) ) & the formula-sort of S = sup the carrier of J & the program-sort of S = (sup the carrier of J) +^ 1 & the carrier of S = the carrier of J \/ { the formula-sort of S, the program-sort of S} & ( for w being Ordinal st w = sup the carrier' of J holds
the carrier' of S = ( the carrier' of J \/ {(w +^ 0),(w +^ 1),(w +^ 2),(w +^ 3),(w +^ 4),(w +^ 5),(w +^ 6),(w +^ 7),(w +^ 8)}) \/ [:{ the carrier' of J},{1,2},X:] ) ) by Th11;
take S ; :: thesis: ( S is J -extension & S is n PC-correct & S is QC-correct & S is n AL-correct )
thus ( S is J -extension & S is n PC-correct & S is QC-correct & S is n AL-correct ) by A1; :: thesis: verum