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

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