let a, b, c, d 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