set X = { k where k is Element of NAT : ( n,k are_coprime & k >= 1 & k <= n ) } ;
{ k where k is Element of NAT : ( n,k are_coprime & k >= 1 & k <= n ) } c= Seg n

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Element of NAT : ( n,k are_coprime & k >= 1 & k <= n ) } or x in Seg n )
assume x in { k where k is Element of NAT : ( n,k are_coprime & k >= 1 & k <= 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 = { k where k is Element of NAT : ( n,k are_coprime & k >= 1 & k <= n ) } as finite set ;
card X is Element of NAT ;
hence card { k where k is Element of NAT : ( n,k are_coprime & k >= 1 & k <= n ) } is Element of NAT ; :: thesis: verum