for a being Ordinal holds not a in dom {} ;
hence ( base- {} = 0 & limit- {} = 0 ) by Def4, Def5; :: thesis: len- {} = 0
hence len- {} = 0 by ORDINAL3:56; :: thesis: verum