let x, y be set ; :: thesis: field {[x,y]} = {x,y}
set R = {[x,y]};
( dom {[x,y]} = {x} & rng {[x,y]} = {y} ) by Th23;
hence field {[x,y]} = {x,y} by ENUMSET1:1; :: thesis: verum