let a, d, b, c be set ; :: thesis: ( not AND3 (AND2 a,d),(AND2 b,d),(AND2 c,d) is empty iff not AND2 (AND3 a,b,c),d is empty )
( not a is empty & not b is empty & not c is empty & not d is empty iff ( not AND3 a,b,c is empty & not d is empty ) ) ;
hence ( not AND3 (AND2 a,d),(AND2 b,d),(AND2 c,d) is empty iff not AND2 (AND3 a,b,c),d is empty ) ; :: thesis: verum