consider u, w being set such that
W0: u in f and
W1: w in f and
W2: u <> w by ZFMISC_1:def 10;
consider u1, u2 being set such that
W3: u = [u1,u2] by W0, RELAT_1:def 1;
consider w1, w2 being set such that
W4: w = [w1,w2] by W1, RELAT_1:def 1;
take u1 ; :: according to ZFMISC_1:def 10 :: thesis: ex b₁ being set 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 W3, W4, W0, W1, RELAT_1:def 4; :: thesis: not u1 = w1
thus u1 <> w1 by W0, W1, W2, W3, W4, Def1; :: thesis: verum