set n = the non empty Nat;
set X = REAL-NS the non empty Nat;
take REAL-NS the non empty Nat ; :: thesis: REAL-NS the non empty Nat is finite-dimensional
thus REAL-NS the non empty Nat is finite-dimensional by Th62; :: thesis: verum