let a, b 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 Th32;
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;