let a, b be natural Ordinal; :: thesis: ( [a,b] in { [a,b] where a, b is Element of omega : ( a,b are_coprime & b <> {} ) } implies ( a,b are_coprime & b <> {} ) )
assume [a,b] in { [a,b] where a, b is Element of omega : ( a,b are_coprime & b <> {} ) } ; :: thesis: ( a,b are_coprime & b <> {} )
then consider c, d being Element of omega such that
A1: [a,b] = [c,d] and
A2: ( c,d are_coprime & d <> {} ) ;
a = c by A1, XTUPLE_0:1;
hence ( a,b are_coprime & b <> {} ) by A1, A2, XTUPLE_0:1; :: thesis: verum