let n be Nat; :: thesis: ( n > 1 implies Euler n <= n - 1 )
set X = { kk where kk is Element of NAT : ( n,kk are_coprime & kk >= 1 & kk <= n ) } ;
{ kk where kk is Element of NAT : ( n,kk are_coprime & kk >= 1 & kk <= n ) } c= Seg n

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { kk where kk is Element of NAT : ( n,kk are_coprime & kk >= 1 & kk <= n ) } or x in Seg n )
assume x in { kk where kk is Element of NAT : ( n,kk are_coprime & kk >= 1 & kk <= n ) } ; :: thesis: x in Seg n
then ex k being Element of NAT st
( k = x & n,k are_coprime & k >= 1 & k <= n ) ;
hence x in Seg n by FINSEQ_1:1; :: thesis: verum

end;

then reconsider X = { kk where kk is Element of NAT : ( n,kk are_coprime & kk >= 1 & kk <= n ) } as finite set ;
assume A1: n > 1 ; :: thesis: Euler n <= n - 1
then 0 in { l where l is Nat : l < n } ;
then 0 in n by AXIOMS:4;
then A2: card (n \ {0}) = (card n) - (card {0}) by Th4;
A3: X c= n \ {0}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in n \ {0} )
assume x in X ; :: thesis: x in n \ {0}
then consider k being Element of NAT such that
A4: k = x and
A5: n,k are_coprime and
A6: k >= 1 and
A7: k <= n ;
not n,n are_coprime by A1, Th1;
then k < n by A5, A7, XXREAL_0:1;
then k in { l where l is Nat : l < n } ;
then A8: k in n by AXIOMS:4;
not k in {0} by A6, TARSKI:def 1;
hence x in n \ {0} by A4, A8, XBOOLE_0:def 5; :: thesis: verum

end;

( card n = n & card {0} = 1 ) by CARD_1:30;
hence Euler n <= n - 1 by A3, A2, NAT_1:43; :: thesis: verum