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 ) } )

proof

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;

1 gcd 1 = 1 by NAT_D:32;
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