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 A3: RED b,a <> 1 ; :: thesis: ( numerator (a / b) = RED a,b & denominator (a / b) = RED b,a )

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

end;

end;