let a, b, x, y be set ; :: thesis: for R being Relation st R = {[a,b],[x,y]} holds
( dom R = {a,x} & rng R = {b,y} )
let R be Relation; :: thesis: ( R = {[a,b],[x,y]} implies ( dom R = {a,x} & rng R = {b,y} ) )
assume A1: R = {[a,b],[x,y]} ; :: thesis: ( dom R = {a,x} & rng R = {b,y} )
thus dom R = {a,x} :: thesis: rng R = {b,y}

proof

thus dom R c= {a,x} :: according to XBOOLE_0:def 10 :: thesis: {a,x} c= dom R

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in dom R or z in {a,x} )
assume z in dom R ; :: thesis: z in {a,x}
then consider c being set such that
A2: [z,c] in R by Def4;
( [z,c] = [a,b] or [z,c] = [x,y] ) by A1, A2, TARSKI:def 2;
then ( z = a or z = x ) by ZFMISC_1:27;
hence z in {a,x} by TARSKI:def 2; :: thesis: verum

end;

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in {a,x} or z in dom R )
assume z in {a,x} ; :: thesis: z in dom R
then ( z = a or z = x ) by TARSKI:def 2;
then ( [z,b] in R or [z,y] in R ) by A1, TARSKI:def 2;
hence z in dom R by Def4; :: thesis: verum

end;

thus rng R c= {b,y} :: according to XBOOLE_0:def 10 :: thesis: {b,y} c= rng R

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng R or z in {b,y} )
assume z in rng R ; :: thesis: z in {b,y}
then consider d being set such that
A3: [d,z] in R by Def5;
( [d,z] = [a,b] or [d,z] = [x,y] ) by A1, A3, TARSKI:def 2;
then ( z = b or z = y ) by ZFMISC_1:27;
hence z in {b,y} by TARSKI:def 2; :: thesis: verum

end;

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in {b,y} or z in rng R )
assume z in {b,y} ; :: thesis: z in rng R
then ( z = b or z = y ) by TARSKI:def 2;
then ( [a,z] in R or [x,z] in R ) by A1, TARSKI:def 2;
hence z in rng R by Def5; :: thesis: verum