theorem :: ARYTM_2:2

omega c= REAL+ by Lm5, Th1;