set i = 4;
consider I being Element 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;
thus not X . 1 is empty by A1; :: thesis: verum