let m be Nat; :: thesis: RelPrimes m c= Seg m
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in RelPrimes m or x in Seg m )
assume x in RelPrimes m ; :: thesis: x in Seg m
then ex k being Element of NAT st
( k = x & m,k are_coprime & k >= 1 & k <= m ) ;
hence x in Seg m ; :: thesis: verum