thus
( x in omega implies ex a being Element of omega st a = 1 )
; ( not x in omega implies ex b1 being Element of omega ex a being natural Ordinal st x = [a,b1] )
assume
not x in omega
; ex b1 being Element of omega ex a being natural Ordinal st x = [a,b1]
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
; ex a being natural Ordinal st x = [a,b]
take
a
; x = [a,b]
thus
x = [a,b]
by A2; verum