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 (DISJOINT_PAIRS A) by A2, FINSUB_1:def 5;

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