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 }
( {} is Element of Fin (DISJOINT_PAIRS A) & ( for a, b being Element of DISJOINT_PAIRS A st a in {} & b in {} & a c= b holds
a = b ) ) by FINSUB_1:7;
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 } ; :: thesis: verum