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 ;
hence contradiction by A1, Def6; :: thesis: verum