let a, b be natural Ordinal; ( b <> {} implies ( numerator (a / b) = RED (a,b) & denominator (a / b) = RED (b,a) ) )
assume A1:
b <> {}
; ( numerator (a / b) = RED (a,b) & denominator (a / b) = RED (b,a) )
per cases
( RED (b,a) = 1 or RED (b,a) <> 1 )
;
suppose A3:
RED (
b,
a)
<> 1
;
( 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;
verum end; end;