set IT = { 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 } ;
{ 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 } c= Fin (DISJOINT_PAIRS A)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x 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 } or x in Fin (DISJOINT_PAIRS A) )
assume x 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: x in Fin (DISJOINT_PAIRS A)
then ex B being Element of Fin (DISJOINT_PAIRS A) st
( x = B & ( for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds
a = b ) ) ;
hence x in Fin (DISJOINT_PAIRS A) ; :: thesis: verum

end;

hence { 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 Subset of (Fin (DISJOINT_PAIRS A)) ; :: thesis: verum