 Types realized in finite structures are principal

Fix a tuple in a finite first-order structure. For every tuple of a different complete type, choose a logical formula true at the first tuple and false at the competitor. The finite conjunction selects only tuples of the desired partial type inside the first-order structure. Every implication from that conjunction to a member of the partial type is true in the first-order structure and hence belongs to its complete theory. Thus the conjunction isolates the partial type, even in an infinite first-order language.