len p = {} ;
then len (FS2XFS p) = {} by Def8;
hence FS2XFS p is empty ; :: thesis: verum