:: deftheorem Def10 defines XOR3 GATE_1:def 10 :
for a, b, c being set holds
( ( ( ( ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) ) & c is empty ) or ( not ( not a is empty & b is empty ) & not ( a is empty & not b is empty ) & not c is empty ) ) implies XOR3 (a,b,c) = NOT1 {} ) & ( ( ( ( not a is empty & b is empty ) or ( a is empty & not b is empty ) ) & c is empty ) or ( not ( not a is empty & b is empty ) & not ( a is empty & not b is empty ) & not c is empty ) or XOR3 (a,b,c) = {} ) );