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