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