let R be Ring; for I being Ideal of R holds
( I is proper iff not R / I is degenerated )
let I be Ideal of R; ( I is proper iff not R / I is degenerated )
set E = EqRel (R,I);
A1:
(1. R) - (0. R) = 1. R
by RLVECT_1:13;
A2:
( 0. (R / I) = Class ((EqRel (R,I)),(0. R)) & 1. (R / I) = Class ((EqRel (R,I)),(1. R)) )
by Def6;
thus
( I is proper implies not R / I is degenerated )
by A2, Th6, A1, IDEAL_1:19; ( not R / I is degenerated implies I is proper )
assume A3:
not R / I is degenerated
; I is proper
assume
not I is proper
; contradiction
then
1. R in I
by IDEAL_1:19;
hence
contradiction
by A2, A1, A3, Th6; verum