:: deftheorem Def3 defines R-orthogonal EUCLID_7:def 3 :
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)| = 0 );