let x be Element of RAT+ ; :: thesis: ex y being Element of RAT+ st x = y + y
set 02 = one + one;
one + one = 1 +^ 1 by Th64;
then one + one <> {} by ORDINAL3:26;
then consider z being Element of RAT+ such that
A1: (one + one) *' z = 1 by Th60;
take y = z *' x; :: thesis: x = y + y
thus x = one *' x by Th59
.= (one + one) *' y by A1, Th58
.= (one *' y) + (one *' y) by Th63
.= y + (one *' y) by Th59
.= y + y by Th59 ; :: thesis: verum