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;