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

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