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