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

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

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

proof

then reconsider X = { k where k is Element of NAT : ( n,k are_coprime & k >= 1 & k <= n ) } as finite set ;
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;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

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