let A be set ; :: thesis: for a being Element of DISJOINT_PAIRS A holds (Atom A) . a = (singleton (DISJOINT_PAIRS A)) . a
let a be Element of DISJOINT_PAIRS A; :: thesis: (Atom A) . a = (singleton (DISJOINT_PAIRS A)) . a
thus (singleton (DISJOINT_PAIRS A)) . a = {a} by SETWISEO:54
.= (Atom A) . a by Def4 ; :: thesis: verum