not omega in omega ;
hence not omega is finite by Lm5; :: thesis: verum