let K be commutative Ring; :: thesis: ( not K is degenerated & K is well-unital & K is Fanoian implies 1_ K <> - (1_ K) )
assume A0: ( not K is degenerated & K is well-unital ) ; :: thesis: ( not K is Fanoian or 1_ K <> - (1_ K) )
assume A1: K is Fanoian ; :: thesis: 1_ K <> - (1_ K)
assume 1_ K = - (1_ K) ; :: thesis: contradiction
then (1_ K) + (1_ K) = 0. K by RLVECT_1:def 10;
hence contradiction by A0, A1; :: thesis: verum