A \ B is Subset of X ;
hence B BUTNOT is List of X ; :: thesis: verum