:: deftheorem Def50 defines -array AOFA_A00:def 50 :
for I, N being set
for n being Nat
for S being ConnectivesSignature holds
( S is n,I,N -array iff ( len the connectives of S >= n + 3 & ex J, K, L being Element of S st
( L = I & K = N & J <> L & J <> K & the connectives of S . n is_of_type <*J,K*>,L & the connectives of S . (n + 1) is_of_type <*J,K,L*>,J & the connectives of S . (n + 2) is_of_type <*J*>,K & the connectives of S . (n + 3) is_of_type <*K,L*>,J ) ) );