let a, b be natural Ordinal; :: thesis: ( [a,b] in RATplus implies ( a,b are_relative_prime & b <> {} ) )
assume [a,b] in RATplus ; :: thesis: ( a,b are_relative_prime & b <> {} )
then consider c, d being Element of omega such that
A1: ( [a,b] = [c,d] & c,d are_relative_prime & d <> {} ) ;
( a = c & b = d ) by A1, ZFMISC_1:33;
hence ( a,b are_relative_prime & b <> {} ) by A1; :: thesis: verum