let a, b, c, d be set ; ( ( AND2 (a,b) is empty implies not OR2 ((NOT1 a),(NOT1 b)) is empty ) & ( not OR2 ((NOT1 a),(NOT1 b)) is empty implies AND2 (a,b) is empty ) & ( not OR2 (a,b) is empty & not OR2 (c,b) is empty implies not OR2 ((AND2 (a,c)),b) is empty ) & ( not OR2 ((AND2 (a,c)),b) is empty implies ( not OR2 (a,b) is empty & not OR2 (c,b) is empty ) ) & ( not OR2 (a,b) is empty & not OR2 (c,b) is empty & not OR2 (d,b) is empty implies not OR2 ((AND3 (a,c,d)),b) is empty ) & ( not OR2 ((AND3 (a,c,d)),b) is empty implies ( not OR2 (a,b) is empty & not OR2 (c,b) is empty & not OR2 (d,b) is empty ) ) & not ( not OR2 (a,b) is empty & ( not a is empty implies not c is empty ) & ( not c is empty implies not a is empty ) & OR2 (c,b) is empty ) )
A1:
( not OR2 (a,b) is empty & not OR2 (c,b) is empty iff ( ( not a is empty or not b is empty ) & ( not c is empty or not b is empty ) ) )
;
A2:
( not OR2 (a,b) is empty & not OR2 (c,b) is empty & not OR2 (d,b) is empty iff ( ( not a is empty or not b is empty ) & ( not c is empty or not b is empty ) & ( not d is empty or not b is empty ) ) )
;
( AND2 (a,b) is empty iff ( a is empty or b is empty ) )
;
hence
( ( AND2 (a,b) is empty implies not OR2 ((NOT1 a),(NOT1 b)) is empty ) & ( not OR2 ((NOT1 a),(NOT1 b)) is empty implies AND2 (a,b) is empty ) & ( not OR2 (a,b) is empty & not OR2 (c,b) is empty implies not OR2 ((AND2 (a,c)),b) is empty ) & ( not OR2 ((AND2 (a,c)),b) is empty implies ( not OR2 (a,b) is empty & not OR2 (c,b) is empty ) ) & ( not OR2 (a,b) is empty & not OR2 (c,b) is empty & not OR2 (d,b) is empty implies not OR2 ((AND3 (a,c,d)),b) is empty ) & ( not OR2 ((AND3 (a,c,d)),b) is empty implies ( not OR2 (a,b) is empty & not OR2 (c,b) is empty & not OR2 (d,b) is empty ) ) & not ( not OR2 (a,b) is empty & ( not a is empty implies not c is empty ) & ( not c is empty implies not a is empty ) & OR2 (c,b) is empty ) )
by A1, A2; verum