len <*x*> = 1 by FINSEQ_1:56;
hence <*x*> is trivial by REALSET1:13; :: thesis: verum