let x be set ; :: thesis: ( x in { k where k is Element of NAT : ( 2,k are_relative_prime & k >= 1 & k <= 2 ) } iff x = 1 )
thus ( x in { k where k is Element of NAT : ( 2,k are_relative_prime & k >= 1 & k <= 2 ) } implies x = 1 ) :: thesis: ( x = 1 implies x in { k where k is Element of NAT : ( 2,k are_relative_prime & k >= 1 & k <= 2 ) } )

proof

assume x in { k where k is Element of NAT : ( 2,k are_relative_prime & k >= 1 & k <= 2 ) } ; :: thesis: x = 1
then consider k being Element of NAT such that
A1: ( k = x & 2,k are_relative_prime ) and
A2: ( k >= 1 & k <= 2 ) ;
A3: 2 gcd 2 = 2 by NAT_D:32;
( k = 1 or k = 2 ) by A2, NAT_1:26;
hence x = 1 by A1, A3, INT_2:def 3; :: thesis: verum

end;

2 gcd 1 = 1 by NEWTON:51;
then 2,1 are_relative_prime by INT_2:def 3;
hence ( x = 1 implies x in { k where k is Element of NAT : ( 2,k are_relative_prime & k >= 1 & k <= 2 ) } ) ; :: thesis: verum