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 ) by A2, Th6, A1, IDEAL_1:19; :: thesis: ( not R / I is degenerated implies I is proper )
assume A3: 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, A3, Th6; :: thesis: verum