let a, b, c, d be set ; :: thesis: ( ( 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; :: thesis: verum

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; :: thesis: verum