take {} ; :: thesis: ( {} is Subset of X & {} is OrthonormalFamily of X & {} is finite )
thus ( {} is Subset of X & {} is OrthonormalFamily of X & {} is finite ) by Th3; :: thesis: verum