let A be set ; :: thesis: {} in { B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds
a = b }
A1: {} is Element of Fin (DISJOINT_PAIRS A) by FINSUB_1:18;
for a, b being Element of DISJOINT_PAIRS A st a in {} & b in {} & a c= b holds
a = b ;
hence {} in { B where B is Element of Fin (DISJOINT_PAIRS A) : for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds
a = b } by A1; :: thesis: verum