let x be object ; :: thesis: ( x in { k where k is Element of NAT : ( 1,k are_coprime & k >= 1 & k <= 1 ) } iff x = 1 )

thus ( x in { k where k is Element of NAT : ( 1,k are_coprime & k >= 1 & k <= 1 ) } implies x = 1 ) :: thesis: ( x = 1 implies x in { k where k is Element of NAT : ( 1,k are_coprime & k >= 1 & k <= 1 ) } )

then 1,1 are_coprime by INT_2:def 3;

hence ( x = 1 implies x in { k where k is Element of NAT : ( 1,k are_coprime & k >= 1 & k <= 1 ) } ) ; :: thesis: verum

thus ( x in { k where k is Element of NAT : ( 1,k are_coprime & k >= 1 & k <= 1 ) } implies x = 1 ) :: thesis: ( x = 1 implies x in { k where k is Element of NAT : ( 1,k are_coprime & k >= 1 & k <= 1 ) } )

proof

1 gcd 1 = 1
by NAT_D:32;
assume
x in { k where k is Element of NAT : ( 1,k are_coprime & k >= 1 & k <= 1 ) }
; :: thesis: x = 1

then ex k being Element of NAT st

( k = x & 1,k are_coprime & k >= 1 & k <= 1 ) ;

hence x = 1 by XXREAL_0:1; :: thesis: verum

end;then ex k being Element of NAT st

( k = x & 1,k are_coprime & k >= 1 & k <= 1 ) ;

hence x = 1 by XXREAL_0:1; :: thesis: verum

then 1,1 are_coprime by INT_2:def 3;

hence ( x = 1 implies x in { k where k is Element of NAT : ( 1,k are_coprime & k >= 1 & k <= 1 ) } ) ; :: thesis: verum