set A = { k where k is Element of NAT : ( 0 ,k are_coprime & k >= 1 & k <= 0 ) } ;
assume Euler 0 <> 0 ; :: thesis: contradiction
then card { k where k is Element of NAT : ( 0 ,k are_coprime & k >= 1 & k <= 0 ) } <> 0 by EULER_1:def 1;
then consider a being object such that
A1: a in { k where k is Element of NAT : ( 0 ,k are_coprime & k >= 1 & k <= 0 ) } by XBOOLE_0:7, CARD_1:27;
ex k being Element of NAT st
( k = a & 0 ,k are_coprime & k >= 1 & k <= 0 ) by A1;
hence contradiction ; :: thesis: verum