let A be set ; :: thesis: for a being Element of DISJOINT_PAIRS A holds a in (Atom A) . a
let a be Element of DISJOINT_PAIRS A; :: thesis: a in (Atom A) . a
(Atom A) . a = {a} by Def4;
hence a in (Atom A) . a by TARSKI:def 1; :: thesis: verum