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
per cases ( 0 = 0. R or 0 = 1. R or ( 0 <> 0. R & 0 <> 1. R ) ) ;
suppose 0 = 0. R ; :: thesis: not R is flat
then the_rank_of (1. R) <> {} by CLASSES1:71;
hence not R is flat by A1, A2; :: thesis: verum
end;
suppose 0 = 1. R ; :: thesis: not R is flat
then the_rank_of (0. R) <> {} by CLASSES1:71;
hence not R is flat by A1, A2; :: thesis: verum
end;
suppose ( 0 <> 0. R & 0 <> 1. R ) ; :: thesis: not R is flat
then the_rank_of (0. R) <> {} by CLASSES1:71;
hence not R is flat by A1, A2; :: thesis: verum
end;
end;