not omega in omega ;
hence not omega is finite by Th103; :: thesis: