let R be commutative Ring; :: thesis: for I being Ideal of R holds
( I is maximal iff R / I is Skew-Field )
let I be Ideal of R; :: thesis: ( I is maximal iff R / I is Skew-Field )
thus ( I is maximal implies R / I is Skew-Field ) by Th16, Th19; :: thesis: ( R / I is Skew-Field implies I is maximal )
assume R / I is Skew-Field ; :: thesis: I is maximal
hence ( I is proper & I is quasi-maximal ) by Th16, Th20; :: according to RING_1:def 4 :: thesis: verum