let X be RealUnitarySpace; :: thesis: for Y being OrthogonalFamily of X
for Z being Subset of X st Z is Subset of Y holds
Z is OrthogonalFamily of X
let Y be OrthogonalFamily of X; :: thesis: for Z being Subset of X st Z is Subset of Y holds
Z is OrthogonalFamily of X
let Z be Subset of X; :: thesis: ( Z is Subset of Y implies Z is OrthogonalFamily of X )
assume Z is Subset of Y ; :: thesis: Z is OrthogonalFamily of X
then for x, y being Point of X 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