let X be RealUnitarySpace; :: thesis: for Y being OrthogonalFamily of X
for Z being Subset of st Z is Subset of holds
Z is OrthogonalFamily of X
let Y be OrthogonalFamily of X; :: thesis: for Z being Subset of st Z is Subset of holds
Z is OrthogonalFamily of X
let Z be Subset of ; :: thesis: ( Z is Subset of implies Z is OrthogonalFamily of X )
assume Z is Subset of ; :: thesis: Z is OrthogonalFamily of X
then for x, y being Point of st x in Z & y in Z & x <> y holds
x .|. y = 0 by BHSP_5:def 8;
hence Z is OrthogonalFamily of X by BHSP_5:def 8; :: thesis: verum