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

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

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

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

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 ) } 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;( ( 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

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

then
M9 is Element of Normal_forms_on A
by Th33;( ( 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;( ( 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

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