theorem Th17: :: EUCLID_7:18

for B0 being Subset of (REAL 0) st B0 is orthogonal_basis holds
B0 = {}