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;