let x be Element of RAT+ ; :: thesis: x *' {} = {}
( numerator {} = {} & (numerator x) *^ {} = {} ) by Def8, Lm1, ORDINAL2:35;
hence x *' {} = {} by Th40; :: thesis: verum