let x1, x2, y1, y2 be object ; :: thesis: ( not {x1,x2} = {y1,y2} or x1 = y1 or x1 = y2 )
x1 in {x1,x2} by TARSKI:def 2;
hence ( not {x1,x2} = {y1,y2} or x1 = y1 or x1 = y2 ) by TARSKI:def 2; :: thesis: verum