set w = sup the carrier' of J;

deffunc H_{1}( ConnectivesSignature ) -> FinSequence of the carrier' of n = the connectives of n;

defpred S_{1}[ Nat, ConnectivesSignature ] means H_{1}(X) . (n + n) = (sup the carrier' of J) +^ n;

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

A2: 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 and

A3: ( ( 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 ) and

( 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;

reconsider S = S as non empty non void J -extension strict n PC-correct QC-correct n AL-correct AlgLangSignature over X by A1;

take S ; :: thesis: S is essential

set c = the connectives of S;

thus the connectives of S .: ((n + 9) \ n) misses the carrier' of J :: according to AOFA_L00:def 18 :: thesis: ( rng the quantifiers of S misses the carrier' of J & { the formula-sort of S, the program-sort of S} misses the carrier of J )

then consider x being object such that

A11: ( x in { the formula-sort of S, the program-sort of S} & x in the carrier of J ) by XBOOLE_0:3;

( x = the formula-sort of S or x = the program-sort of S ) by A11, TARSKI:def 2;

then ( sup the carrier of J in sup the carrier of J or (sup the carrier of J) +^ 1 in sup the carrier of J ) by A3, A11, ORDINAL2:19;

then (sup the carrier of J) +^ 1 in (sup the carrier of J) +^ 0 by ORDINAL2:27;

hence contradiction by ORDINAL3:22; :: thesis: verum

deffunc H

defpred S

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

A2: 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 and

A3: ( ( 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 ) and

( 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;

reconsider S = S as non empty non void J -extension strict n PC-correct QC-correct n AL-correct AlgLangSignature over X by A1;

take S ; :: thesis: S is essential

set c = the connectives of S;

thus the connectives of S .: ((n + 9) \ n) misses the carrier' of J :: according to AOFA_L00:def 18 :: thesis: ( rng the quantifiers of S misses the carrier' of J & { the formula-sort of S, the program-sort of S} misses the carrier of J )

proof

thus
rng the quantifiers of S misses the carrier' of J
:: thesis: { the formula-sort of S, the program-sort of S} misses the carrier of J
assume
the connectives of S .: ((n + 9) \ n) meets the carrier' of J
; :: thesis: contradiction

then consider x being object such that

A4: ( x in the connectives of S .: ((n + 9) \ n) & x in the carrier' of J ) by XBOOLE_0:3;

consider k being object such that

A5: ( k in dom the connectives of S & k in (n + 9) \ n & x = the connectives of S . k ) by A4, FUNCT_1:def 6;

reconsider k = k as Nat by A5;

set k1 = k -' n;

A6: ( k in Segm (n + 9) & k nin n ) by A5, XBOOLE_0:def 5;

then Segm n c= Segm k by ORDINAL1:16;

then ( n <= k & k < (n + 8) + 1 ) by A6, NAT_1:44;

then ( n <= k & k <= n + 8 ) by NAT_1:13;

then A7: ( n + 0 <= n + (k -' n) & n + (k -' n) <= n + 8 & k = n + (k -' n) ) by XREAL_1:235;

then ( 0 <= k -' n & k -' n <= 8 ) by XREAL_1:6;

then not not 0 = k -' n & ... & not 8 = k -' n ;

then the connectives of S . k = (sup the carrier' of J) +^ (k -' n) by A2, A7;

then ( (sup the carrier' of J) +^ (k -' n) in sup the carrier' of J & sup the carrier' of J = (sup the carrier' of J) +^ 0 ) by A4, A5, ORDINAL2:19, ORDINAL2:27;

hence contradiction by ORDINAL3:22; :: thesis: verum

end;then consider x being object such that

A4: ( x in the connectives of S .: ((n + 9) \ n) & x in the carrier' of J ) by XBOOLE_0:3;

consider k being object such that

A5: ( k in dom the connectives of S & k in (n + 9) \ n & x = the connectives of S . k ) by A4, FUNCT_1:def 6;

reconsider k = k as Nat by A5;

set k1 = k -' n;

A6: ( k in Segm (n + 9) & k nin n ) by A5, XBOOLE_0:def 5;

then Segm n c= Segm k by ORDINAL1:16;

then ( n <= k & k < (n + 8) + 1 ) by A6, NAT_1:44;

then ( n <= k & k <= n + 8 ) by NAT_1:13;

then A7: ( n + 0 <= n + (k -' n) & n + (k -' n) <= n + 8 & k = n + (k -' n) ) by XREAL_1:235;

then ( 0 <= k -' n & k -' n <= 8 ) by XREAL_1:6;

then not not 0 = k -' n & ... & not 8 = k -' n ;

then the connectives of S . k = (sup the carrier' of J) +^ (k -' n) by A2, A7;

then ( (sup the carrier' of J) +^ (k -' n) in sup the carrier' of J & sup the carrier' of J = (sup the carrier' of J) +^ 0 ) by A4, A5, ORDINAL2:19, ORDINAL2:27;

hence contradiction by ORDINAL3:22; :: thesis: verum

proof

assume
{ the formula-sort of S, the program-sort of S} meets the carrier of J
; :: thesis: contradiction
assume
rng the quantifiers of S meets the carrier' of J
; :: thesis: contradiction

then consider x being object such that

A8: ( x in rng the quantifiers of S & x in the carrier' of J ) by XBOOLE_0:3;

consider y being object such that

A9: ( y in dom the quantifiers of S & x = the quantifiers of S . y ) by A8, FUNCT_1:def 3;

dom the quantifiers of S = [: the quant-sort of S,X:] by FUNCT_2:def 1

.= [:{1,2},X:] by Def5 ;

then consider i, z being object such that

A10: ( i in {1,2} & z in X & y = [i,z] ) by A9, ZFMISC_1:def 2;

( i = 1 or i = 2 ) by A10, TARSKI:def 2;

then ( x = the quantifiers of S . (i,z) & the quantifiers of S . (i,z) = [ the carrier' of J,i,z] ) by A9, A10, A3;

then ( the carrier' of J in { the carrier' of J} & { the carrier' of J} in {{ the carrier' of J,i},{ the carrier' of J}} & {{ the carrier' of J,i},{ the carrier' of J}} in {[ the carrier' of J,i]} & {[ the carrier' of J,i]} in the quantifiers of S . (i,z) & the quantifiers of S . (i,z) = x & x in the carrier' of J ) by A8, TARSKI:def 1, TARSKI:def 2;

hence contradiction by XREGULAR:9; :: thesis: verum

end;then consider x being object such that

A8: ( x in rng the quantifiers of S & x in the carrier' of J ) by XBOOLE_0:3;

consider y being object such that

A9: ( y in dom the quantifiers of S & x = the quantifiers of S . y ) by A8, FUNCT_1:def 3;

dom the quantifiers of S = [: the quant-sort of S,X:] by FUNCT_2:def 1

.= [:{1,2},X:] by Def5 ;

then consider i, z being object such that

A10: ( i in {1,2} & z in X & y = [i,z] ) by A9, ZFMISC_1:def 2;

( i = 1 or i = 2 ) by A10, TARSKI:def 2;

then ( x = the quantifiers of S . (i,z) & the quantifiers of S . (i,z) = [ the carrier' of J,i,z] ) by A9, A10, A3;

then ( the carrier' of J in { the carrier' of J} & { the carrier' of J} in {{ the carrier' of J,i},{ the carrier' of J}} & {{ the carrier' of J,i},{ the carrier' of J}} in {[ the carrier' of J,i]} & {[ the carrier' of J,i]} in the quantifiers of S . (i,z) & the quantifiers of S . (i,z) = x & x in the carrier' of J ) by A8, TARSKI:def 1, TARSKI:def 2;

hence contradiction by XREGULAR:9; :: thesis: verum

then consider x being object such that

A11: ( x in { the formula-sort of S, the program-sort of S} & x in the carrier of J ) by XBOOLE_0:3;

( x = the formula-sort of S or x = the program-sort of S ) by A11, TARSKI:def 2;

then ( sup the carrier of J in sup the carrier of J or (sup the carrier of J) +^ 1 in sup the carrier of J ) by A3, A11, ORDINAL2:19;

then (sup the carrier of J) +^ 1 in (sup the carrier of J) +^ 0 by ORDINAL2:27;

hence contradiction by ORDINAL3:22; :: thesis: verum