let A be set ; :: thesis: {[{},{}]} is Element of Normal_forms_on A
[{},{}] is Element of DISJOINT_PAIRS A by Th12;
then {[{},{}]} c= DISJOINT_PAIRS A by ZFMISC_1:31;
then reconsider B = {[{},{}]} as Element of Fin (DISJOINT_PAIRS A) by FINSUB_1:def 5;
now :: thesis: for a, b being Element of DISJOINT_PAIRS A st a in B & b in B & a c= b holds
a = b
let a, b be Element of DISJOINT_PAIRS A; :: thesis: ( a in B & b in B & a c= b implies a = b )
assume that
A1: a in B and
A2: b in B and
a c= b ; :: thesis: a = b
a = [{},{}] by A1, TARSKI:def 1;
hence a = b by A2, TARSKI:def 1; :: thesis: verum
end;
hence {[{},{}]} is Element of Normal_forms_on A by NORMFORM:33; :: thesis: verum