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

proof

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

end;

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