( 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_{1} being non empty non void strict ConnectivesSignature st

( b_{1} is 1,I,N -array & b_{1} is 4 -connectives )
; :: thesis: verum

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

( b