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