set K = INT.Ring ;
take INT.Ring ; :: thesis: ( INT.Ring is Fanoian & not INT.Ring is degenerated & INT.Ring is well-unital & INT.Ring is domRing-like & INT.Ring is commutative )
INT.Ring is Fanoian
proof
let a be Element of INT.Ring; :: according to VECTSP_1:def 17 :: thesis: ( not a + a = 0. INT.Ring or a = 0. INT.Ring )
assume A1: a + a = 0. INT.Ring ; :: thesis: a = 0. INT.Ring
reconsider aa = a as Element of INT ;
aa + aa = 0. INT.Ring by BINOP_2:def 20, A1;
then 2 * aa = 0 ;
then aa = 0 ;
then a = 0. INT.Ring ;
hence a = 0. INT.Ring ; :: thesis: verum
end;
hence ( INT.Ring is Fanoian & not INT.Ring is degenerated & INT.Ring is well-unital & INT.Ring is domRing-like & INT.Ring is commutative ) ; :: thesis: verum