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 that
A1: {x,y} \ X <> {} and
A2: {x,y} \ X <> {x} and
A3: {x,y} \ X <> {y} ; :: thesis: {x,y} \ X = {x,y}
A4: ( ( not x in X & x <> y ) or y in X ) by A3, Lm12;
( x in X or ( not y in X & x <> y ) ) by A2, Lm12;
hence {x,y} \ X = {x,y} by A1, A4, Th72, Th73; :: thesis: verum