let a be Element of DISJOINT_PAIRS {}; :: thesis: a = [{},{}]
consider x, y being Element of Fin {} such that
A1: a = [x,y] by DOMAIN_1:1;
x = {} by FINSUB_1:15, TARSKI:def 1;
hence a = [{},{}] by A1, FINSUB_1:15, TARSKI:def 1; :: thesis: verum