let x be Element of RAT+ ; :: thesis: denominator x <> {}
per cases ( x in omega or not x in omega ) ;
suppose x in omega ; :: thesis: denominator x <> {}
hence denominator x <> {} by Def9, Lm4; :: thesis: verum
end;
suppose A1: not x in omega ; :: thesis: denominator x <> {}
then ex i, j being Element of omega st
( x = [i,j] & i,j are_coprime & j <> {} & j <> 1 ) by Th29;
hence denominator x <> {} by A1, Def9; :: thesis: verum
end;
end;