set S = R / ([#] R);
set I = [#] R;
now :: thesis: for x, y being Element of (R / ([#] R)) holds x = y
let x, y be Element of (R / ([#] R)); :: thesis: x = y
consider a being Element of R such that
H1: x = Class ((EqRel (R,([#] R))),a) by RING_1:11;
consider b being Element of R such that
H2: y = Class ((EqRel (R,([#] R))),b) by RING_1:11;
thus x = the carrier of R by H1, RING_1:7
.= y by H2, RING_1:7 ; :: thesis: verum
end;
hence R / ([#] R) is trivial ; :: thesis: verum