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