let R be Ring; :: thesis: for I being Ideal of R holds
( I is proper iff not R / I is degenerated )
let I be Ideal of R; :: thesis: ( 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 ) :: thesis: ( not R / I is degenerated implies I is proper )

proof

assume that
A3: I is proper and
A4: 0. (R / I) = 1. (R / I) ; :: according to STRUCT_0:def 8 :: thesis: contradiction
(1. R) - (0. R) in I by A2, A4, Th6;
hence contradiction by A1, A3, IDEAL_1:19; :: thesis: verum

end;

assume A5: not R / I is degenerated ; :: thesis: I is proper
assume not I is proper ; :: thesis: contradiction
then 1. R in I by IDEAL_1:19;
hence contradiction by A2, A1, A5, Th6; :: thesis: verum