let x, y, X be set ; :: thesis: ( {x,y} \ X = {} or {x,y} \ X = {x} or {x,y} \ X = {y} or {x,y} \ X = {x,y} )
assume ( {x,y} \ X <> {} & {x,y} \ X <> {x} & {x,y} \ X <> {y} ) ; :: thesis: {x,y} \ X = {x,y}
then ( ( not x in X or not y in X ) & ( x in X or ( not y in X & x <> y ) ) & ( ( not x in X & x <> y ) or y in X ) ) by Lm12, Th73;
hence {x,y} \ X = {x,y} by Th72; :: thesis: verum