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

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