let b, a be natural Ordinal; :: thesis: ( b <> {} implies ( numerator (a / b) = RED a,b & denominator (a / b) = RED b,a ) )
assume A1: b <> {} ; :: thesis: ( numerator (a / b) = RED a,b & denominator (a / b) = RED b,a )

per cases ( RED b,a = 1 or RED b,a <> 1 ) ;

suppose A2: RED b,a = 1 ; :: thesis: ( numerator (a / b) = RED a,b & denominator (a / b) = RED b,a )

then a / b = RED a,b by Def10;
hence ( numerator (a / b) = RED a,b & denominator (a / b) = RED b,a ) by A2, Def8, Def9; :: thesis: verum

end;

suppose RED b,a <> 1 ; :: thesis: ( numerator (a / b) = RED a,b & denominator (a / b) = RED b,a )

then ( a / b = [(RED a,b),(RED b,a)] & not [(RED a,b),(RED b,a)] in omega ) by A1, Def10, Th38;
hence ( numerator (a / b) = RED a,b & denominator (a / b) = RED b,a ) by Def8, Def9; :: thesis: verum

end;

end;