( I in {I,N} & N in {I,N} ) by TARSKI:def 2;
then ex C being non empty non void strict 4 -connectives ConnectivesSignature st
( C is 1,I,N -array & C is 1-1-connectives & {I,N} c= the carrier of C & {} misses the carrier' of C & the ResultSort of C . ( the connectives of C . 2) nin {I,N} ) by Th52;
hence ex b₁ being non empty non void strict ConnectivesSignature st
( b₁ is 1,I,N -array & b₁ is 4 -connectives ) ; :: thesis: verum