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] and
A2: ( c,d are_relative_prime & d <> {} ) ;
a = c by A1, ZFMISC_1:27;
hence ( a,b are_relative_prime & b <> {} ) by A1, A2, ZFMISC_1:27; :: thesis: verum