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

( 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