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 { [a,b] where a, b is Element of omega : ( a,b are_coprime & b <> {} ) } \ { [k,1] where k is Element of omega : verum } by XBOOLE_0:def 3;
then x in { [a,b] where a, b is Element of omega : ( a,b are_coprime & b <> {} ) } ;
then consider a, b being Element of omega such that
A2: x = [a,b] and
a,b are_coprime and
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