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

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