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