let R be Ring; :: thesis: ( R is degenerated implies R is almost_trivial )
assume A1: R is degenerated ; :: thesis: R is almost_trivial
now :: thesis: for a being Element of R holds
( a = 1. R or a = 0. R )
let a be Element of R; :: thesis: ( a = 1. R or a = 0. R )
a = a * (1. R)
.= a * (0. R) by A1, STRUCT_0:def 8
.= 0. R ;
hence ( a = 1. R or a = 0. R ) ; :: thesis: verum
end;
hence R is almost_trivial ; :: thesis: verum