theorem :: EUCLID_7:15

for B0 being set holds
( B0 is R-orthogonal iff for x, y being real-valued FinSequence st x in B0 & y in B0 & x <> y holds
x,y are_orthogonal )