let I be Ideal of R; :: thesis: ( I is maximal implies I is prime )

assume A1: ( I is proper & I is quasi-maximal ) ; :: according to RING_1:def 4 :: thesis: I is prime

then ( R / I is almost_left_invertible & not R / I is degenerated ) by Th16, Th19;

hence ( I is proper & I is quasi-prime ) by A1, Th17; :: according to RING_1:def 2 :: thesis: verum

assume A1: ( I is proper & I is quasi-maximal ) ; :: according to RING_1:def 4 :: thesis: I is prime

then ( R / I is almost_left_invertible & not R / I is degenerated ) by Th16, Th19;

hence ( I is proper & I is quasi-prime ) by A1, Th17; :: according to RING_1:def 2 :: thesis: verum