let X1, X2, X3, X4 be set ; ( ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} ) iff [:X1,X2,X3,X4:] <> {} )
A1:
[:[:X1,X2,X3:],X4:] = [:X1,X2,X3,X4:]
by ZFMISC_1:def 4;
( ( X1 <> {} & X2 <> {} & X3 <> {} ) iff [:X1,X2,X3:] <> {} )
by Th21;
hence
( ( X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} ) iff [:X1,X2,X3,X4:] <> {} )
by A1, ZFMISC_1:90; verum