let L be Ring; :: thesis: ( L is degenerated iff the carrier of L = {(0. L)} )

now :: thesis: ( L is degenerated implies the carrier of L = {(0. L)} )

assume AS: L is degenerated ; :: thesis: the carrier of L = {(0. L)}
B: {(0. L)} c= the carrier of L ;

now :: thesis: for o being object st o in the carrier of L holds
o in {(0. L)}

let o be object ; :: thesis: ( o in the carrier of L implies o in {(0. L)} )
assume o in the carrier of L ; :: thesis: o in {(0. L)}
then reconsider a = o as Element of L ;
a = a * (1. L)
.= 0. L by AS ;
hence o in {(0. L)} by TARSKI:def 1; :: thesis: verum

end;

hence the carrier of L = {(0. L)} by B, TARSKI:2; :: thesis: verum

end;

hence ( L is degenerated iff the carrier of L = {(0. L)} ) ; :: thesis: verum