let A be set ; :: thesis: {[{} ,{} ]} is Element of Normal_forms_on A
[{} ,{} ] is Element of DISJOINT_PAIRS A by Th17;
then ( {[{} ,{} ]} is finite & {[{} ,{} ]} c= DISJOINT_PAIRS A ) by ZFMISC_1:37;
then reconsider B = {[{} ,{} ]} as Element of Fin (DISJOINT_PAIRS A) by FINSUB_1:def 5;

now

let a, b be Element of DISJOINT_PAIRS A; :: thesis: ( a in B & b in B & a c= b implies a = b )
assume ( a in B & b in B & a c= b ) ; :: thesis: a = b
then ( a = [{} ,{} ] & b = [{} ,{} ] ) by TARSKI:def 1;
hence a = b ; :: thesis: verum

end;

hence {[{} ,{} ]} is Element of Normal_forms_on A by NORMFORM:53; :: thesis: verum