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