let R be Ring; for I being Ideal of R st R / I is almost_left_invertible holds
I is quasi-maximal
let I be Ideal of R; ( R / I is almost_left_invertible implies I is quasi-maximal )
set E = EqRel (R,I);
assume A1:
R / I is almost_left_invertible
; I is quasi-maximal
given J being Ideal of R such that A2:
I c= J
and
A3:
J <> I
and
A4:
J is proper
; RING_1:def 3 contradiction
not J c= I
by A2, A3;
then consider a being object such that
A5:
a in J
and
A6:
not a in I
;
reconsider a = a as Element of R by A5;
reconsider x = Class ((EqRel (R,I)),a) as Element of (R / I) by Th12;
A7:
Class ((EqRel (R,I)),(0. R)) = 0. (R / I)
by Def6;
then consider y being Element of (R / I) such that
A8:
y * x = 1. (R / I)
by A1;
consider b being Element of R such that
A9:
y = Class ((EqRel (R,I)),b)
by Th11;
A10:
Class ((EqRel (R,I)),(1. R)) = 1. (R / I)
by Def6;
y * x = Class ((EqRel (R,I)),(b * a))
by A9, Th14;
then A11:
(b * a) - (1. R) in I
by A10, A8, Th6;
A12:
1. R = (b * a) - ((b * a) - (1. R))
by Th2;
b * a in J
by A5, IDEAL_1:def 2;
then
1. R in J
by A2, A11, A12, IDEAL_1:15;
hence
contradiction
by A4, IDEAL_1:19; verum