OuterVx f,n c= Seg n by Th29;
hence OuterVx f,n is finite ; :: thesis: verum