( a c= b or b c= a ) ;
hence not a *` b is finite by Th27; :: thesis: verum