set M = { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t )
}
;
now :: thesis: for x being object st x in { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t )
}
holds
x in B
let x be object ; :: thesis: ( x in { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t )
}
implies x in B )

assume x in { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t )
}
; :: thesis: x in B
then ex t being Element of DISJOINT_PAIRS A st
( x = t & ( for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t ) ) ) ;
hence x in B ; :: thesis: verum
end;
then A1: { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t ) } c= B ;
then A2: { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t ) } is finite by FINSET_1:1;
B c= DISJOINT_PAIRS A by FINSUB_1:def 5;
then { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t ) } c= DISJOINT_PAIRS A by A1;
then reconsider M9 = { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t )
}
as Element of Fin () by ;
now :: thesis: for c, d being Element of DISJOINT_PAIRS A st c in { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t )
}
& d in { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t )
}
& c c= d holds
c = d
let c, d be Element of DISJOINT_PAIRS A; :: thesis: ( c in { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t )
}
& d in { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t )
}
& c c= d implies c = d )

assume c in { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t )
}
; :: thesis: ( d in { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t )
}
& c c= d implies c = d )

then ex t being Element of DISJOINT_PAIRS A st
( c = t & ( for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t ) ) ) ;
then A3: c in B ;
assume d in { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t )
}
; :: thesis: ( c c= d implies c = d )
then ex t being Element of DISJOINT_PAIRS A st
( d = t & ( for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t ) ) ) ;
hence ( c c= d implies c = d ) by A3; :: thesis: verum
end;
then M9 is Element of Normal_forms_on A by Th33;
hence { t where t is Element of DISJOINT_PAIRS A : for s being Element of DISJOINT_PAIRS A holds
( ( s in B & s c= t ) iff s = t ) } is Element of Normal_forms_on A ; :: thesis: verum