consider u, w being object such that
A1: u in f and
A2: w in f and
A3: u <> w by ZFMISC_1:def 10;
consider u1, u2 being object such that
A4: u = [u1,u2] by A1, RELAT_1:def 1;
consider w1, w2 being object such that
A5: w = [w1,w2] by A2, RELAT_1:def 1;
take u1 ; :: according to ZFMISC_1:def 10 :: thesis: ex b₁ being object st
( u1 in dom f & b₁ in dom f & not u1 = b₁ )
take w1 ; :: thesis: ( u1 in dom f & w1 in dom f & not u1 = w1 )
thus ( u1 in dom f & w1 in dom f ) by A4, A5, A1, A2, XTUPLE_0:def 12; :: thesis: not u1 = w1
thus u1 <> w1 by A1, A2, A3, A4, A5, Def1; :: thesis: verum