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

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

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

2 gcd 1 = 1
by NEWTON:51;
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;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

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