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