let B be Orthogonal_Basis of n; :: thesis: not B is empty
assume A1: B is empty ; :: thesis: contradiction
then B c= RN_Base n by XBOOLE_1:2;
hence contradiction by Def7, A1; :: thesis: verum