let X be set ; :: thesis: {} is Subset of X
{} X = {} ;
hence {} is Subset of X ; :: thesis: verum