thus ( x in omega implies ex a being Element of omega st a = x ) ; :: thesis: ( not x in omega implies ex b₁ being Element of omega ex a being natural Ordinal st x = [b₁,a] )
assume not x in omega ; :: thesis: ex b₁ being Element of omega ex a being natural Ordinal st x = [b₁,a]
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
A1: x = [a,b] and
a,b are_coprime and
b <> {} ;
take a ; :: thesis: ex a being natural Ordinal st x = [a,a]
take b ; :: thesis: x = [a,b]
thus x = [a,b] by A1; :: thesis: verum