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