let a, b be set ; :: thesis: ( ( not XOR3 a,b,{} is empty implies not XOR2 a,b is empty ) & ( not XOR2 a,b is empty implies not XOR3 a,b,{} is empty ) & ( not XOR3 a,{} ,b is empty implies not XOR2 a,b is empty ) & ( not XOR2 a,b is empty implies not XOR3 a,{} ,b is empty ) & ( not XOR3 {} ,a,b is empty implies not XOR2 a,b is empty ) & ( not XOR2 a,b is empty implies not XOR3 {} ,a,b is empty ) )
( ( XOR3 a,b,{} is empty or ( not a is empty & b is empty ) or ( a is empty & not b is empty ) ) & ( ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) ) implies not XOR3 a,b,{} is empty ) & ( XOR3 a,{} ,b is empty or ( not a is empty & b is empty ) or ( a is empty & not b is empty ) ) & ( ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) ) implies not XOR3 a,{} ,b is empty ) & ( XOR3 {} ,a,b is empty or ( not a is empty & b is empty ) or ( a is empty & not b is empty ) ) & ( ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) ) implies not XOR3 {} ,a,b is empty ) ) ;
hence ( ( not XOR3 a,b,{} is empty implies not XOR2 a,b is empty ) & ( not XOR2 a,b is empty implies not XOR3 a,b,{} is empty ) & ( not XOR3 a,{} ,b is empty implies not XOR2 a,b is empty ) & ( not XOR2 a,b is empty implies not XOR3 a,{} ,b is empty ) & ( not XOR3 {} ,a,b is empty implies not XOR2 a,b is empty ) & ( not XOR2 a,b is empty implies not XOR3 {} ,a,b is empty ) ) ; :: thesis: verum