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

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