let a, b, c be object ; :: according to FUNCT_1:def 1 :: thesis: ( not [a,b] in {[x,y],[y,x]} or not [a,c] in {[x,y],[y,x]} or b = c )
assume ( [a,b] in {[x,y],[y,x]} & [a,c] in {[x,y],[y,x]} ) ; :: thesis: b = c
then ( ( [a,b] = [x,y] or [a,b] = [y,x] ) & ( [a,c] = [x,y] or [a,c] = [y,x] ) ) by TARSKI:def 2;
then ( ( ( a = x & b = y ) or ( a = y & b = x ) ) & ( ( a = x & c = y ) or ( a = y & c = x ) ) ) by XTUPLE_0:1;
hence b = c ; :: thesis: verum