let x be Element of RAT+ ; ( x in omega or ex i, j being Element of omega st
( x = [i,j] & i,j are_coprime & j <> {} & j <> 1 ) )
assume
not x in omega
; ex i, j being Element of omega st
( x = [i,j] & i,j are_coprime & j <> {} & j <> 1 )
then A1:
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 A2:
not x in { [k,1] where k is Element of omega : verum }
by XBOOLE_0:def 5;
x in { [a,b] where a, b is Element of omega : ( a,b are_coprime & b <> {} ) }
by A1;
then consider a, b being Element of omega such that
A3:
( x = [a,b] & a,b are_coprime & b <> {} )
;
[a,1] in { [k,1] where k is Element of omega : verum }
;
hence
ex i, j being Element of omega st
( x = [i,j] & i,j are_coprime & j <> {} & j <> 1 )
by A2, A3; verum