Bags X c= Bags X ;
hence Bags X is Subset of (Bags X) ; :: thesis: verum