let a be set ; :: thesis: {a} is mutually-disjoint
let x, y be set ; :: according to TAXONOM2:def 5 :: thesis: ( x in {a} & y in {a} & x <> y implies x misses y )
assume that
A1: x in {a} and
A2: y in {a} and
A3: x <> y ; :: thesis: x misses y
x = a by A1, TARSKI:def 1;
hence x misses y by A2, A3, TARSKI:def 1; :: thesis: verum