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)

a = b } is Subset of (Fin (DISJOINT_PAIRS A)) ; :: thesis: verum

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

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
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;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

a = b } is Subset of (Fin (DISJOINT_PAIRS A)) ; :: thesis: verum