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

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