take {} ; :: thesis: ( {} is Subset of X & {} is OrthogonalFamily of X & ( for x being Point of X st x in {} holds
x .|. x = 1 ) )
thus ( {} is Subset of X & {} is OrthogonalFamily of X & ( for x being Point of X st x in {} holds
x .|. x = 1 ) ) by Th2; :: thesis: verum