let R be Ring; :: thesis: for I being Ideal of R st R / I is almost_left_invertible holds
I is quasi-maximal
let I be Ideal of R; :: thesis: ( R / I is almost_left_invertible implies I is quasi-maximal )
set E = EqRel (R,I);
assume A1: R / I is almost_left_invertible ; :: thesis: 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 ; :: according to RING_1:def 3 :: thesis: 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;

now :: thesis: not x = 0. (R / I)

assume x = 0. (R / I) ; :: thesis: contradiction
then a - (0. R) in I by A7, Th6;
hence contradiction by A6, RLVECT_1:13; :: thesis: verum

end;

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; :: thesis: verum