let x, y be object ; :: thesis: for X being set holds
( {x,y} \ X = {} or {x,y} \ X = {x} or {x,y} \ X = {y} or {x,y} \ X = {x,y} )
let 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, Lm11;
( x in X or ( not y in X & x <> y ) ) by A2, Lm11;
hence {x,y} \ X = {x,y} by A1, A4, Th50, Th63, XBOOLE_1:83; :: thesis: verum