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:9;
x = {} by FINSUB_1:28, TARSKI:def 1;
hence a = [{} ,{} ] by A1, FINSUB_1:28, TARSKI:def 1; :: thesis: verum