let x, y, z be object ; :: thesis: ( {x,y} c= {z} implies {x,y} = {z} )
assume {x,y} c= {z} ; :: thesis: {x,y} = {z}
then ( x = z & y = z ) by Th20;
hence {x,y} = {z} by ENUMSET1:29; :: thesis: verum