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