let x be Element of RAT+ ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum