let x, y be object ; 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 ; ( {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}
; {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; verum