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, XBOOLE_0:def 10;
then consider a being set such that
A5: a in J and
A6: not a in I by TARSKI:def 3;
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

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

end;

then consider y being Element of (R / I) such that
A8: y * x = 1. (R / I) by A1, VECTSP_1:def 20;
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