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: 0. (R / I) = Class (EqRel R,I),(0. R) by Def6;
A2: 1. (R / I) = Class (EqRel R,I),(1. R) by Def6;
A3: (1. R) - (0. R) = 1. R by RLVECT_1:26;
thus ( I is proper implies not R / I is degenerated ) :: thesis: ( not R / I is degenerated implies I is proper )

proof

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

end;

assume A6: 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;
then Class (EqRel R,I),(1. R) = Class (EqRel R,I),(0. R) by A3, Th6;
hence contradiction by A1, A2, A6; :: thesis: verum