consider I being SortSymbol of S such that

A1: I = 1 and

( I <> the bool-sort of S & the connectives of S . 4 is_of_type {} ,I & the connectives of S . (4 + 1) is_of_type {} ,I & the connectives of S . 4 <> the connectives of S . (4 + 1) & the connectives of S . (4 + 2) is_of_type <*I*>,I & the connectives of S . (4 + 3) is_of_type <*I,I*>,I & the connectives of S . (4 + 4) is_of_type <*I,I*>,I & the connectives of S . (4 + 5) is_of_type <*I,I*>,I & the connectives of S . (4 + 3) <> the connectives of S . (4 + 4) & the connectives of S . (4 + 3) <> the connectives of S . (4 + 5) & the connectives of S . (4 + 4) <> the connectives of S . (4 + 5) & the connectives of S . (4 + 6) is_of_type <*I,I*>, the bool-sort of S ) by Def38;

take I ; :: thesis: I is integer

thus I = 1 by A1; :: according to AOFA_A00:def 39 :: thesis: verum

A1: I = 1 and

( I <> the bool-sort of S & the connectives of S . 4 is_of_type {} ,I & the connectives of S . (4 + 1) is_of_type {} ,I & the connectives of S . 4 <> the connectives of S . (4 + 1) & the connectives of S . (4 + 2) is_of_type <*I*>,I & the connectives of S . (4 + 3) is_of_type <*I,I*>,I & the connectives of S . (4 + 4) is_of_type <*I,I*>,I & the connectives of S . (4 + 5) is_of_type <*I,I*>,I & the connectives of S . (4 + 3) <> the connectives of S . (4 + 4) & the connectives of S . (4 + 3) <> the connectives of S . (4 + 5) & the connectives of S . (4 + 4) <> the connectives of S . (4 + 5) & the connectives of S . (4 + 6) is_of_type <*I,I*>, the bool-sort of S ) by Def38;

take I ; :: thesis: I is integer

thus I = 1 by A1; :: according to AOFA_A00:def 39 :: thesis: verum