consider J, K, L being Element of S such that
A1: ( L = 1 & K = 1 & J <> L & J <> K & the connectives of S . 11 is_of_type <*J,K*>,L & the connectives of S . (11 + 1) is_of_type <*J,K,L*>,J & the connectives of S . (11 + 2) is_of_type <*J*>,K & the connectives of S . (11 + 3) is_of_type <*K,L*>,J ) by Def50;
take K ; :: thesis: K is integer
thus K = 1 by A1; :: according to AOFA_A00:def 39 :: thesis: verum