let R be non degenerated Ring; :: thesis: ( 0 in the carrier of R implies not R is flat )

A1: the_rank_of 0 = 0 by CLASSES1:71;

assume A2: 0 in the carrier of R ; :: thesis: not R is flat

A1: the_rank_of 0 = 0 by CLASSES1:71;

assume A2: 0 in the carrier of R ; :: thesis: not R is flat