thus ( x in omega implies ex a being Element of omega st a = 1 ) ; :: thesis: ( not x in omega implies ex b₁ being Element of omega ex a being natural Ordinal st x = [a,b₁] )
assume not x in omega ; :: thesis: ex b₁ being Element of omega ex a being natural Ordinal st x = [a,b₁]
then x in RATplus \ { [k,1] where k is Element of omega : verum } by XBOOLE_0:def 3;
then x in RATplus ;
then consider a, b being Element of omega such that
A2: ( x = [a,b] & a,b are_relative_prime & b <> {} ) ;
take b ; :: thesis: ex a being natural Ordinal st x = [a,b]
take a ; :: thesis: x = [a,b]
thus x = [a,b] by A2; :: thesis: verum