let C be non void Signature; :: thesis: for o being OperSymbol of C holds
( ( o is nullary implies not o is unary ) & ( o is nullary implies not o is binary ) & ( o is unary implies not o is binary ) )
let o be OperSymbol of C; :: thesis: ( ( o is nullary implies not o is unary ) & ( o is nullary implies not o is binary ) & ( o is unary implies not o is binary ) )
thus ( o is nullary implies not o is unary ) :: thesis: ( ( o is nullary implies not o is binary ) & ( o is unary implies not o is binary ) )

proof

assume the_arity_of o = {} ; :: according to ABCMIZ_A:def 13 :: thesis: not o is unary
hence len (the_arity_of o) <> 1 ; :: according to ABCMIZ_A:def 14 :: thesis: verum

end;

thus ( o is nullary implies not o is binary ) :: thesis: ( o is unary implies not o is binary )

proof

assume the_arity_of o = {} ; :: according to ABCMIZ_A:def 13 :: thesis: not o is binary
hence len (the_arity_of o) <> 2 ; :: according to ABCMIZ_A:def 15 :: thesis: verum

end;

assume len (the_arity_of o) = 1 ; :: according to ABCMIZ_A:def 14 :: thesis: not o is binary
hence len (the_arity_of o) <> 2 ; :: according to ABCMIZ_A:def 15 :: thesis: verum