:: deftheorem Def10 defines flat FIELD_3:def 11 :
for R being Ring holds
( R is flat iff for a, b being Element of R holds the_rank_of a = the_rank_of b );